diff options
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 45 |
1 files changed, 12 insertions, 33 deletions
diff --git a/Makefile.checker b/Makefile.checker index 3d1d251701..a0f0778d49 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -22,7 +22,7 @@ CHICKEN:=bin/coqchk$(EXE) # The sources -CHKLIBS:= -I config -I clib -I lib -I checker +CHKLIBS:= -I config -I clib -I lib -I checker -I kernel -I kernel/byterun ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread @@ -34,22 +34,9 @@ CHECKMLLIBFILE := checker/.mllibfiles CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE)) -include $(CHECKERDEPS) -# Copied files -checker/esubst.mli: kernel/esubst.mli - cp -a $< $@ - sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak -checker/esubst.ml: kernel/esubst.ml - cp -a $< $@ - sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak -checker/names.mli: kernel/names.mli - cp -a $< $@ - sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak -checker/names.ml: kernel/names.ml - cp -a $< $@ - sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak - ifeq ($(BEST),opt) -$(CHICKEN): config/config.cmxa checker/check.cmxa checker/coqchk.mli checker/coqchk.ml +$(CHICKEN): config/config.cmxa clib/clib.cmxa lib/lib.cmxa kernel/kernel.cmxa \ +checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP_HIDE) $@ @@ -59,30 +46,29 @@ $(CHICKEN): $(CHICKENBYTE) cp $< $@ endif -$(CHICKENBYTE): config/config.cma checker/check.cma checker/coqchk.mli checker/coqchk.ml +$(CHICKENBYTE): config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma \ +checker/check.cma $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ + $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) -cclib -lcoqrun $(VMBYTEFLAGS) -o $@ $^ -checker/check.cma: checker/check.mllib | md5chk +checker/check.cma: checker/check.mllib $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) -checker/check.cmxa: checker/check.mllib | md5chk +checker/check.cmxa: checker/check.mllib $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml) - -CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKGENFILES) \ +CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) \ $(filter dev/checker_%, $(MLFILES) $(MLIFILES)) -$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES)) +$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(TOTARGET) -$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP) +$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP) $(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES' - $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) $(TOTARGET) + $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) checker/%.cmi: checker/%.mli $(SHOW)'OCAMLC $<' @@ -104,13 +90,6 @@ dev/checker_%.cmi: dev/checker_%.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< -md5chk: - $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml" >&2; false; fi - -.PHONY: md5chk - # For emacs: # Local Variables: # mode: makefile |