From bfbcd1e3feeaa7eb24c15686439926c536c5d483 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Dec 2019 01:32:10 +0100
Subject: [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.
---
 .gitignore    |  1 +
 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:
-- 
cgit v1.2.3