From 861a83842efcb536e9ffdd0ba7173621daab47a4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 23 Aug 2019 20:47:39 +0200
Subject: [ci] [dune] Updates to dune builds artifacts.

Closes #10694

We modify handling of artifacts for dune builds:
- we preserve `_build/log` log as artifact for ci-builds,
- we use a tar.gz as to preserve file permissions which is necessary
  in order to reuse the artifacts in an incremental build.

Dune uses this rule to digest a file:

```
  Digest.generic (file_contents f, f.stats.st_perm land 0o100 (* Only take USR_X in account *))
```

Since a few releases, Gitlab CI uses `.zip` as the storage format for
artifacts, this means that files in `_build` will get the executable
bit set when they did not have it originally, making all the digest
cache to miss. This caused #10694 .

See https://gitlab.com/gitlab-org/gitlab/issues/18711
---
 .gitlab-ci.yml | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 935d5fda84..956d74c8c1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -103,13 +103,16 @@ before_script:
     - set -e
     - make -f Makefile.dune world
     - set +e
+    - tar cfj _build.tar.bz2 _build
   variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
   artifacts:
     name: "$CI_JOB_NAME"
+    when: always
     paths:
-      - _build/
+      - _build/log
+      - _build.tar.bz2
     expire_in: 1 week
 
 .dune-ci-template:
@@ -119,6 +122,7 @@ before_script:
   dependencies:
     - build:edge+flambda:dune:dev
   script:
+    - tar xfj _build.tar.bz2
     - set -e
     - echo 'start:coq.test'
     - make -f Makefile.dune "$DUNE_TARGET"
@@ -128,6 +132,7 @@ before_script:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
   artifacts:
+    when: always
     name: "$CI_JOB_NAME"
     expire_in: 2 months
 
@@ -409,6 +414,7 @@ doc:refman:dune:
     DUNE_TARGET: refman-html
   artifacts:
     paths:
+      - _build/log
       - _build/default/doc/sphinx_build/html
 
 doc:stdlib:dune:
@@ -417,6 +423,7 @@ doc:stdlib:dune:
     DUNE_TARGET: stdlib-html
   artifacts:
     paths:
+      - _build/log
       - _build/default/doc/stdlib/html
 
 doc:refman:deploy:
@@ -456,6 +463,7 @@ doc:ml-api:odoc:
     DUNE_TARGET: apidoc
   artifacts:
     paths:
+      - _build/log
       - _build/default/_doc/
 
 test-suite:base:
@@ -486,13 +494,15 @@ test-suite:edge+flambda:
     OPAM_VARIANT: "+flambda"
   only: *full-ci
 
-test-suite:egde:dune:dev:
+test-suite:edge:dune:dev:
   stage: stage-2
   dependencies:
     - build:edge+flambda:dune:dev
   needs:
     - build:edge+flambda:dune:dev
-  script: make -f Makefile.dune test-suite
+  script:
+    - tar xfj _build.tar.bz2
+    - make -f Makefile.dune test-suite
   variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
-- 
cgit v1.2.3


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


From d21e17ac99dfb2008f2e2bfdb373413490d1ffc7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Dec 2019 10:32:13 +0100
Subject: [make] Add _build_boot to find_skip_dirs

---
 Makefile.make | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile.make b/Makefile.make
index c7d162bc56..d8e229e4db 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -56,6 +56,7 @@ FIND_SKIP_DIRS:='(' \
   -name "$${GIT_DIR}" -o \
   -name '_build' -o \
   -name '_build_ci' -o \
+  -name '_build_boot' -o \
   -name '_install_ci' -o \
   -name 'gramlib' -o \
   -name 'user-contrib' -o \
-- 
cgit v1.2.3