Merge PR #13467: [ci] add job for interval

Reviewed-by: SkySkimmer
Ack-by: silene

8 files changed, 79 insertions, 14 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 875f713a1c..ddbace193a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -738,7 +738,14 @@ library:ci-coqtail:
   extends: .ci-template
 
 library:ci-coquelicot:
-  extends: .ci-template
+  stage: stage-3
+  extends: .ci-template-flambda
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
 
 library:ci-cross_crypto:
   extends: .ci-template
@@ -792,6 +799,42 @@ library:ci-flocq:
 library:ci-menhir:
   extends: .ci-template-flambda
 
+library:ci-interval:
+  extends: .ci-template-flambda
+  stage: stage-4
+  needs:
+  - build:edge+flambda
+  - library:ci-coquelicot
+  - library:ci-flocq
+  - library:ci-mathcomp
+  - plugin:ci-bignums
+  dependencies:
+  - build:edge+flambda
+  - library:ci-coquelicot
+  - library:ci-flocq
+  - library:ci-mathcomp
+  - plugin:ci-bignums
+
+library:ci-oddorder:
+  extends: .ci-template-flambda
+  stage: stage-3
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
+
+library:ci-fourcolor:
+  extends: .ci-template-flambda
+  stage: stage-3
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
+
 library:ci-corn:
   extends: .ci-template-flambda
   stage: stage-4
diff --git a/Makefile.ci b/Makefile.ci
index 759462f509..9f08de662f 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -34,15 +34,18 @@ CI_TARGETS= \
     ci-fiat_crypto_ocaml \
     ci-fiat_parsers \
     ci-flocq \
+    ci-fourcolor \
     ci-geocoq \
     ci-coqhammer \
     ci-hott \
+    ci-interval \
     ci-iris \
     ci-math_classes \
     ci-mathcomp \
     ci-menhir \
     ci-metacoq \
     ci-mtac2 \
+    ci-oddorder \
     ci-paramcoq \
     ci-perennial \
     ci-quickchick \
@@ -69,7 +72,7 @@ ci-all: $(CI_TARGETS)
 ci-color: ci-bignums
 
 ci-coqprime: ci-bignums
-
+ci-coquelicot: ci-mathcomp
 ci-math_classes: ci-bignums
 
 ci-corn: ci-math_classes
@@ -79,6 +82,10 @@ ci-mtac2: ci-unicoq
 ci-fiat_crypto: ci-coqprime ci-rewriter
 ci-fiat_crypto_ocaml: ci-fiat_crypto
 
+ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums
+ci-fourcolor: ci-mathcomp
+ci-oddorder: ci-mathcomp
+
 ci-simple_io: ci-ext_lib
 ci-quickchick: ci-ext_lib ci-simple_io
 
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index ffe92dcecf..777d36a6d7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-install_ssreflect
-
 git_download coquelicot
 
-( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/coquelicot" && ( if [ ! -x ./configure ]; then autoreconf -i -s && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index a3a704091b..cb6c3e6452 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download flocq
 
-( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-fourcolor.sh b/dev/ci/ci-fourcolor.sh
new file mode 100755
index 0000000000..72a1567398
--- /dev/null
+++ b/dev/ci/ci-fourcolor.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download fourcolor
+
+( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh
new file mode 100755
index 0000000000..fe7b3f9fbe
--- /dev/null
+++ b/dev/ci/ci-interval.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download interval
+
+export COQEXTRAFLAGS='-native-compiler no'
+( cd "${CI_BUILD_DIR}/interval" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh
index b1aa56ec4e..f170b35327 100755
--- a/dev/ci/ci-mathcomp.sh
+++ b/dev/ci/ci-mathcomp.sh
@@ -7,11 +7,3 @@ ci_dir="$(dirname "$0")"
 git_download mathcomp
 
 ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install )
-
-git_download fourcolor
-
-( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
-
-git_download oddorder
-
-( cd "${CI_BUILD_DIR}/oddorder" && make )
diff --git a/dev/ci/ci-oddorder.sh b/dev/ci/ci-oddorder.sh
new file mode 100755
index 0000000000..b2da32ad61
--- /dev/null
+++ b/dev/ci/ci-oddorder.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download oddorder
+
+( cd "${CI_BUILD_DIR}/oddorder" && make && make install )