From b75018e36899e939de25509a579385967b9a7010 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 Nov 2017 14:24:54 +0100
Subject: Do dependencies in 1 command per file class.

---
 Makefile.build                                     | 45 +++++++++++++---------
 Makefile.checker                                   | 22 ++++++-----
 .../timing/after/time-of-build-after.log.desired   |  3 +-
 .../timing/after/time-of-build-before.log.desired  |  3 +-
 tools/CoqMakefile.in                               | 11 +++---
 5 files changed, 47 insertions(+), 37 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 39b793d2bb..cf052ebec5 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)
@@ -670,21 +676,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
@@ -756,9 +765,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 435d8e8f64..2fa9a73357 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/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 729de2f366..7900c034da 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 b25bc3683c..7ab0bc75d9 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 4ee6efec0c..a674426f52 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -228,8 +228,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) \
@@ -307,7 +308,7 @@ else
 DO_NATDYNLINK =
 endif
 
-ALLDFILES = $(addsuffix .d,$(ALLSRCFILES))
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE))
 
 # Compilation targets #########################################################
 
@@ -712,9 +713,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 ########################################################################
 
-- 
cgit v1.2.3


From 23e503c15cbb2602507e5afb95590f8bdc0af134 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Nov 2017 15:06:41 +0100
Subject: Overlay for unimath.

---
 dev/ci/user-overlays/06217-coqdep-at-once.sh | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 dev/ci/user-overlays/06217-coqdep-at-once.sh

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 0000000000..68e1901f7f
--- /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
-- 
cgit v1.2.3