1 files changed, 88 insertions, 0 deletions
diff --git a/checker/Makefile b/checker/Makefile
new file mode 100644
index 00000000..2bcc9d36
--- /dev/null
+++ b/checker/Makefile
@@ -0,0 +1,88 @@
+OCAMLC=ocamlc
+OCAMLOPT=ocamlopt
+
+COQSRC=..
+
+MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4
+BYTEFLAGS=$(MLDIRS)
+OPTFLAGS=$(MLDIRS)
+
+CHECKERNAME=coqchk
+
+BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
+MCHECKERLOCAL :=\
+  declarations.cmo environ.cmo \
+  closure.cmo reduction.cmo \
+  type_errors.cmo \
+  modops.cmo \
+  inductive.cmo typeops.cmo \
+  indtypes.cmo subtyping.cmo mod_checking.cmo \
+validate.cmo \
+  safe_typing.cmo check.cmo \
+  check_stat.cmo checker.cmo
+
+MCHECKER:=\
+  $(COQSRC)/config/coq_config.cmo \
+  $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
+  $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
+  $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
+  $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
+  $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
+  $(COQSRC)/kernel/esubst.cmo term.cmo \
+  $(MCHECKERLOCAL)
+
+all: $(BINARIES)
+
+byte : ../bin/$(CHECKERNAME)$(EXE)
+opt : ../bin/$(CHECKERNAME).opt$(EXE)
+
+check.cma: $(MCHECKERLOCAL)
+	ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
+
+check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
+	ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
+
+../bin/$(CHECKERNAME)$(EXE): check.cma
+	ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml
+
+../bin/$(CHECKERNAME).opt$(EXE): check.cmxa
+	ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml
+
+stats:
+	@echo STRUCTURE
+	@wc names.ml term.ml declarations.ml environ.ml type_errors.ml
+	@echo
+	@echo REDUCTION
+	@-wc esubst.ml closure.ml reduction.ml
+	@echo
+	@echo TYPAGE
+	@wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml
+	@echo
+	@echo MODULES
+	@wc modops.ml subtyping.ml
+	@echo
+	@echo INTERFACE
+	@wc check*.ml main.ml 
+	@echo
+	@echo TOTAL
+	@wc *.ml | tail -1
+
+.SUFFIXES:.ml .mli .cmi .cmo .cmx
+
+.ml.cmo:
+	$(OCAMLC) -c $(BYTEFLAGS) $<
+
+.ml.cmx:
+	$(OCAMLOPT) -c $(OPTFLAGS) $<
+
+.mli.cmi:
+	$(OCAMLC) -c $(BYTEFLAGS) $<
+
+
+depend::
+	ocamldep *.ml* > .depend
+
+clean::
+	rm -f *.cm* *.o *.a *~ $(BINARIES)
+
+-include .depend