[CI] Remove Stdlib dep from mathcomp

Following math-comp/math-comp#1343

Author: proux01

.gitlab-ci.yml

@@ -809,7 +809,6 @@ library:ci-oddorder:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
   stage: build-3+
@@ -818,7 +817,6 @@ library:ci-fourcolor:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
   stage: build-3+
@@ -856,15 +854,13 @@ library:ci-mathcomp:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb  # for Hierarchy Builder
   stage: build-2
 
 library:ci-mathcomp_test:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
   stage: build-3+
@@ -892,7 +888,6 @@ library:ci-finmap:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
   stage: build-3+
@@ -901,7 +896,6 @@ library:ci-bigenough:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
   stage: build-3+
@@ -910,13 +904,24 @@ library:ci-analysis:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
   - library:ci-mathcomp
   - library:ci-finmap
   - library:ci-bigenough
   - plugin:ci-elpi_hb  # for Hierarchy Builder
   stage: build-3+
 
+library:ci-analysis_stdlib:
+  extends: .ci-template-flambda
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  - library:ci-finmap
+  - library:ci-bigenough
+  - library:ci-analysis
+  - plugin:ci-elpi_hb  # for Hierarchy Builder
+  - library:ci-stdlib+flambda
+  stage: build-3+
+
 library:ci-neural_net_interp:
   extends: .ci-template
   needs:
@@ -1119,7 +1124,6 @@ plugin:ci-elpi_hb:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - library:ci-stdlib+flambda
 
 plugin:ci-elpi_test:
   extends: .ci-template-flambda

Makefile.ci

@@ -32,6 +32,7 @@ CI_PLATFORM_FULL= \
     ci-finmap \
     ci-bigenough \
     ci-analysis \
+    ci-analysis_stdlib \
     ci-menhir \
     ci-mtac2 \
     ci-paramcoq \
@@ -140,8 +141,8 @@ ci-lean_importer: ci-stdlib
 ci-mathcomp: ci-elpi_hb
 
 ci-coqprime: ci-bignums
-ci-coquelicot: ci-mathcomp
-ci-deriving: ci-mathcomp
+ci-coquelicot: ci-mathcomp ci-stdlib
+ci-deriving: ci-mathcomp ci-stdlib
 ci-math_classes: ci-bignums
 
 ci-coqhammer: ci-stdlib
@@ -172,22 +173,22 @@ ci-fiat_parsers: ci-stdlib
 
 ci-fourcolor: ci-mathcomp
 ci-oddorder: ci-mathcomp
-ci-fcsl_pcm: ci-mathcomp
-ci-mczify: ci-mathcomp
+ci-fcsl_pcm: ci-mathcomp ci-stdlib
+ci-mczify: ci-mathcomp ci-stdlib
 ci-algebra_tactics: ci-mczify
 ci-mathcomp_test: ci-mathcomp
-ci-mathcomp_word: ci-mathcomp
+ci-mathcomp_word: ci-mathcomp ci-stdlib
 ci-finmap: ci-mathcomp
 ci-bigenough: ci-mathcomp
 ci-analysis: ci-elpi_hb ci-finmap ci-bigenough
+ci-analysis_stdlib: ci-analysis ci-stdlib
 
 ci-hb: ci-elpi
 
-ci-elpi: ci-stdlib
-ci-elpi_test: ci-elpi
+ci-elpi_test: ci-elpi ci-stdlib
 ci-hb_test: ci-hb
 
-ci-trakt: ci-elpi
+ci-trakt: ci-elpi ci-stdlib
 
 ci-engine_bench: ci-stdlib
 

dev/ci/scripts/ci-analysis.sh

@@ -10,6 +10,12 @@ git_download analysis
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/analysis"
-  make
-  make install
+  make -C classical
+  make -C classical install
+  make -C reals
+  make -C reals install
+  make -C theories
+  make -C theories install
+  make -C experimental_reals
+  make -C experimental_reals install
 )

dev/ci/scripts/ci-analysis_stdlib.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+set -e
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
+
+( cd "${CI_BUILD_DIR}/analysis"
+  make -C reals_stdlib
+  make -C reals_stdlib install
+  make -C analysis_stdlib
+  make -C analysis_stdlib install
+)

dev/ci/scripts/ci-elpi_test.sh

@@ -9,7 +9,6 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/elpi"
   export DUNE_build_FLAGS="--release"
-  make test-core
-  make examples
-  make test-apps
+  make -j1 all-tests
+  make -j1 all-examples
 )