diff options
| -rw-r--r-- | Makefile.build | 45 | ||||
| -rw-r--r-- | Makefile.checker | 22 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06217-coqdep-at-once.sh | 3 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-after.log.desired | 3 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-before.log.desired | 3 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 11 |
6 files changed, 50 insertions, 37 deletions
diff --git a/Makefile.build b/Makefile.build index 940943c41..3411e062e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -147,8 +147,14 @@ endif # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +VDFILE := .vfiles +MLDFILE := .mlfiles +PLUGMLDFILE := plugins/.mlfiles +MLLIBDFILE := .mllibfiles +PLUGMLLIBDFILE := plugins/.mllibfiles + DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLDFILE) $(MLLIBDFILE) $(PLUGMLDFILE) $(PLUGMLLIBDFILE) $(CFILES) $(VDFILE)) -include $(DEPENDENCIES) @@ -189,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile -LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) +LOCALINCLUDES=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) @@ -197,7 +203,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) -DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils) +DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/utils) # On MacOS, the binaries are signed, except our private ones ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) @@ -671,21 +677,24 @@ plugins/%.cmx: plugins/%.ml # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) +MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) + +$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP MLFILES MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(MAINMLFILES) $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP MLLIBFILES MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(MAINMLLIBFILES) $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP plugins/MLFILES plugins/MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(TOTARGET) -%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) ########################################################################### # Compilation of .v files @@ -757,9 +766,9 @@ endif # Dependencies of .v files -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) +$(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) $(VFILES) $(TOTARGET) ########################################################################### diff --git a/Makefile.checker b/Makefile.checker index b14f705be..73d47dfae 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -26,6 +26,12 @@ CHKLIBS:= -I config -I lib -I checker # The rules +CHECKMLDFILE := checker/.mlfiles +CHECKMLLIBFILE := checker/.mllibfiles + +CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE)) +-include $(CHECKERDEPS) + ifeq ($(BEST),opt) $(CHICKEN): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' @@ -49,17 +55,13 @@ checker/check.cmxa: checker/check.mllib | md5chk $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -checker/%.ml.d: checker/%.ml - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) - -checker/%.mli.d: checker/%.mli - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) +$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) + $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET) -checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET) +$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP) + $(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) checker/%.cmi: checker/%.mli $(SHOW)'OCAMLC $<' diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh new file mode 100644 index 000000000..68e1901f7 --- /dev/null +++ b/dev/ci/user-overlays/06217-coqdep-at-once.sh @@ -0,0 +1,3 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then + UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git +fi diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 729de2f36..7900c034d 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index b25bc3683..7ab0bc75d 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 2b56c63a0..33a2f8593 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -227,8 +227,9 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules +VDFILE := .coqdeps + ALLSRCFILES := \ - $(VFILES) \ $(ML4FILES) \ $(MLFILES) \ $(MLPACKFILES) \ @@ -308,7 +309,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) # Compilation targets ######################################################### @@ -713,9 +714,9 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) +$(VDFILE).d: $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) # Misc ######################################################################## |