From c2b9df20204a60bc23535648ff772c4faab45851 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 22 Aug 2019 18:42:01 +0200
Subject: [gitlab/ci] Deploy sooner thanks to new needs keyword.

---
 .gitlab-ci.yml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7c9a5c9a31..e6eba7745a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -367,7 +367,8 @@ pkg:nix:deploy:channel:
   only:
     variables:
       - $CACHIX_DEPLOYMENT_KEY
-  dependencies:
+  dependencies: []
+  needs:
     - pkg:nix:deploy
   script:
     - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
@@ -414,6 +415,10 @@ doc:refman:deploy:
     - doc:ml-api:odoc
     - doc:refman:dune
     - doc:stdlib:dune
+  needs:
+    - doc:ml-api:odoc
+    - doc:refman:dune
+    - doc:stdlib:dune
   script:
     - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
     - git clone git@github.com:coq/doc.git _deploy
-- 
cgit v1.2.3


From 45db028fa0ffbdd77cf87dc73f9d59d488e1c7b6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 22 Aug 2019 18:52:21 +0200
Subject: [gitlab/ci] Build Bignums only once.

We go back to the kind of workflow we had in CircleCI thanks to GitLab
12.2 new needs keyword.
---
 .gitlab-ci.yml | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e6eba7745a..0501de8534 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,6 +4,8 @@ stages:
   - docker
   - build
   - test
+  - test-with-deps-1
+  - test-with-deps-2
   - deploy
 
 # some default values
@@ -589,6 +591,13 @@ library:ci-bedrock2:
 
 library:ci-color:
   extends: .ci-template-flambda
+  stage: test-with-deps-1
+  needs:
+  - build:edge+flambda
+  - plugin:ci-bignums
+  dependencies:
+  - build:edge+flambda
+  - plugin:ci-bignums
 
 library:ci-compcert:
   extends: .ci-template-flambda
@@ -613,6 +622,13 @@ library:ci-flocq:
 
 library:ci-corn:
   extends: .ci-template-flambda
+  stage: test-with-deps-2
+  needs:
+  - build:edge+flambda
+  - library:ci-math-classes
+  dependencies:
+  - build:edge+flambda
+  - library:ci-math-classes
 
 library:ci-geocoq:
   extends: .ci-template-flambda
@@ -623,6 +639,20 @@ library:ci-hott:
 library:ci-iris-lambda-rust:
   extends: .ci-template-flambda
 
+library:ci-math-classes:
+  extends: .ci-template-flambda
+  stage: test-with-deps-1
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
+  needs:
+  - build:edge+flambda
+  - plugin:ci-bignums
+  dependencies:
+  - build:edge+flambda
+  - plugin:ci-bignums
+
 library:ci-math-comp:
   extends: .ci-template-flambda
 
@@ -647,7 +677,11 @@ plugin:ci-aac_tactics:
   extends: .ci-template
 
 plugin:ci-bignums:
-  extends: .ci-template
+  extends: .ci-template-flambda
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
 
 plugin:ci-coq_dpdgraph:
   extends: .ci-template
-- 
cgit v1.2.3


From 0fc73b31859abb42f3fccf018497b33dfa49c33b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 22 Aug 2019 19:06:32 +0200
Subject: [gitlab/ci] Do not wait for all builds to finish to run the tests.

---
 .gitlab-ci.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0501de8534..c46e56c721 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -110,6 +110,8 @@ before_script:
 
 .dune-ci-template:
   stage: test
+  needs:
+    - build:edge+flambda:dune:dev
   dependencies:
     - build:edge+flambda:dune:dev
   script:
@@ -192,11 +194,15 @@ before_script:
     - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
     - echo 'end:coq.test'
     - set +e
+  needs:
+    - build:base
   dependencies:
     - build:base
 
 .ci-template-flambda:
   extends: .ci-template
+  needs:
+    - build:edge+flambda
   dependencies:
     - build:edge+flambda
   variables:
-- 
cgit v1.2.3


From a580f0f072e614b4713b91ae1e033fed7e20f053 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 23 Aug 2019 17:44:28 +0200
Subject: [gitlab/ci] Rework stages, always use needs keyword.

Now everything that does not have any dependencies goes to the first stage.
The rest goes to the first stage following all its dependencies.
All jobs specifying a dependencies keyword also specify a needs keyword.
---
 .gitlab-ci.yml | 69 ++++++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 46 insertions(+), 23 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c46e56c721..ce0c1d9af7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -2,12 +2,15 @@ image: "$IMAGE"
 
 stages:
   - docker
-  - build
-  - test
-  - test-with-deps-1
-  - test-with-deps-2
+  - stage-1 # No dependencies
+  - stage-2 # Only dependencies in stage 1
+  - stage-3 # Only dependencies in stage 1 and 2
+  - stage-4 # Only dependencies in stage 1, 2 and 3
   - deploy
 
+# When a job has no dependencies, it goes to stage 1.
+# Otherwise, we set "needs" and "dependencies" to the same value.
+
 # some default values
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
@@ -55,7 +58,7 @@ before_script:
 
 # TODO figure out how to build doc for installed Coq
 .build-template:
-  stage: build
+  stage: stage-1
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
@@ -93,7 +96,7 @@ before_script:
 
 # Template for building Coq + stdlib, typical use: overload the switch
 .dune-template:
-  stage: build
+  stage: stage-1
   dependencies: []
   script:
     - set -e
@@ -109,7 +112,7 @@ before_script:
     expire_in: 1 week
 
 .dune-ci-template:
-  stage: test
+  stage: stage-2
   needs:
     - build:edge+flambda:dune:dev
   dependencies:
@@ -133,7 +136,7 @@ before_script:
 # overridden otherwise the CI will fail.
 
 .doc-template:
-  stage: test
+  stage: stage-2
   dependencies:
     - not-a-real-job
   script:
@@ -148,7 +151,7 @@ before_script:
 
 # set dependencies when using
 .test-suite-template:
-  stage: test
+  stage: stage-2
   dependencies:
     - not-a-real-job
   script:
@@ -171,7 +174,7 @@ before_script:
 
 # set dependencies when using
 .validate-template:
-  stage: test
+  stage: stage-2
   dependencies:
     - not-a-real-job
   script:
@@ -187,7 +190,7 @@ before_script:
     expire_in: 2 months
 
 .ci-template:
-  stage: test
+  stage: stage-2
   script:
     - set -e
     - echo 'start:coq.test'
@@ -210,7 +213,7 @@ before_script:
     OPAM_VARIANT: "+flambda"
 
 .windows-template:
-  stage: test
+  stage: stage-1
   artifacts:
     name: "%CI_JOB_NAME%"
     paths:
@@ -269,7 +272,7 @@ build:edge+flambda:dune:dev:
 
 build:base+async:
   extends: .build-template
-  stage: test
+  stage: stage-1
   variables:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
     COQUSERFLAGS: "-async-proofs on"
@@ -303,7 +306,7 @@ windows32:
     - /^pr-.*$/
 
 lint:
-  stage: test
+  stage: stage-1
   script: dev/lint-repository.sh
   dependencies: []
   variables:
@@ -311,7 +314,7 @@ lint:
     OPAM_SWITCH: base
 
 pkg:opam:
-  stage: test
+  stage: stage-1
   # OPAM will build out-of-tree so no point in importing artifacts
   dependencies: []
   script:
@@ -328,7 +331,7 @@ pkg:opam:
 
 .nix-template:
   image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
-  stage: test
+  stage: stage-1
   variables:
     # By default we use coq.cachix.org as an extra substituter but this can be overridden
     EXTRA_SUBSTITUTERS: https://coq.cachix.org
@@ -394,6 +397,8 @@ doc:refman:
   extends: .doc-template
   dependencies:
     - build:base
+  needs:
+    - build:base
 
 doc:refman:dune:
   extends: .dune-ci-template
@@ -454,11 +459,15 @@ test-suite:base:
   extends: .test-suite-template
   dependencies:
     - build:base
+  needs:
+    - build:base
 
 test-suite:base+32bit:
   extends: .test-suite-template
   dependencies:
     - build:base+32bit
+  needs:
+    - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
   only: *full-ci
@@ -467,15 +476,19 @@ test-suite:edge+flambda:
   extends: .test-suite-template
   dependencies:
     - build:edge+flambda
+  needs:
+    - build:edge+flambda
   variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
   only: *full-ci
 
 test-suite:egde:dune:dev:
-  stage: test
+  stage: stage-2
   dependencies:
     - build:edge+flambda:dune:dev
+  needs:
+    - build:edge+flambda:dune:dev
   script: make -f Makefile.dune test-suite
   variables:
     OPAM_SWITCH: edge
@@ -489,7 +502,7 @@ test-suite:egde:dune:dev:
     # expire_in: never
 
 test-suite:edge+trunk+make:
-  stage: test
+  stage: stage-1
   dependencies: []
   script:
     - opam switch create 4.09.0 --empty
@@ -516,7 +529,7 @@ test-suite:edge+trunk+make:
   only: *full-ci
 
 test-suite:edge+trunk+dune:
-  stage: test
+  stage: stage-1
   dependencies: []
   script:
     - opam switch create 4.09.0 --empty
@@ -548,6 +561,8 @@ test-suite:base+async:
   extends: .test-suite-template
   dependencies:
     - build:base
+  needs:
+    - build:base
   variables:
     COQFLAGS: "-async-proofs on -async-proofs-cache force"
     timeout: "timeout 100m"
@@ -560,11 +575,15 @@ validate:base:
   extends: .validate-template
   dependencies:
     - build:base
+  needs:
+    - build:base
 
 validate:base+32bit:
   extends: .validate-template
   dependencies:
     - build:base+32bit
+  needs:
+    - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
   only: *full-ci
@@ -573,6 +592,8 @@ validate:edge+flambda:
   extends: .validate-template
   dependencies:
     - build:edge+flambda
+  needs:
+    - build:edge+flambda
   variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
@@ -582,6 +603,8 @@ validate:quick:
   extends: .validate-template
   dependencies:
     - build:quick
+  needs:
+    - build:quick
   only:
     variables:
       - $UNRELIABLE =~ /enabled/
@@ -597,7 +620,7 @@ library:ci-bedrock2:
 
 library:ci-color:
   extends: .ci-template-flambda
-  stage: test-with-deps-1
+  stage: stage-3
   needs:
   - build:edge+flambda
   - plugin:ci-bignums
@@ -628,7 +651,7 @@ library:ci-flocq:
 
 library:ci-corn:
   extends: .ci-template-flambda
-  stage: test-with-deps-2
+  stage: stage-4
   needs:
   - build:edge+flambda
   - library:ci-math-classes
@@ -647,7 +670,7 @@ library:ci-iris-lambda-rust:
 
 library:ci-math-classes:
   extends: .ci-template-flambda
-  stage: test-with-deps-1
+  stage: stage-3
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
@@ -711,7 +734,7 @@ plugin:ci-paramcoq:
   extends: .ci-template
 
 plugin:plugin-tutorial:
-  stage: test
+  stage: stage-1
   dependencies: []
   script:
     - ./configure -local -warn-error yes
-- 
cgit v1.2.3