diff options
| author | Emilio Jesus Gallego Arias | 2019-12-09 01:32:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-16 10:31:45 +0100 |
| commit | bfbcd1e3feeaa7eb24c15686439926c536c5d483 (patch) | |
| tree | bf97d766e395c7c9c8ffea433e19c1b2476462f1 | |
| parent | 861a83842efcb536e9ffdd0ba7173621daab47a4 (diff) | |
[dune] Use a special directory for the boot build
This is related to and fixes #10694 in part.
When calling bootstrap in an incremental build step, we must be sure
the generated dune files are in place. In the CI, these won't be in
place, so we must bootstrap without altering the digest and trace
database coming from the artifact.
Using a separate boot step to recreate the missing `dune` files works
fine and takes just a few seconds.
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Makefile.dune | 11 |
2 files changed, 7 insertions, 5 deletions
diff --git a/.gitignore b/.gitignore index 6c117028a9..12a5c11e5e 100644 --- a/.gitignore +++ b/.gitignore @@ -52,6 +52,7 @@ TAGS bin/ _build_ci _build +_build_boot config/Makefile config/coq_config.ml config/coq_config.py diff --git a/Makefile.dune b/Makefile.dune index 19e8a770bd..bafb40d55f 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -11,7 +11,8 @@ # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short -BUILD_CONTEXT=_build/default +BOOT_DIR=_build_boot +BOOT_CONTEXT=$(BOOT_DIR)/default help: @echo "Welcome to Coq's Dune-based build system. Targets are:" @@ -45,8 +46,8 @@ plugins/ltac/dune: @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune voboot: plugins/ltac/dune - dune build $(DUNEOPT) @vodeps - dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d + dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps + dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d states: voboot dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude @@ -104,8 +105,8 @@ ocheck: voboot ireport: dune clean - dune build $(DUNEOPT) @vodeps --profile=ireport - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d --profile=ireport + dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps + dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d dune build $(DUNEOPT) @install --profile=ireport clean: |