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