[ci] add job for interval

3 files changed, 27 insertions, 0 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6b58676af0..32299d49d6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -792,6 +792,22 @@ library:ci-flocq:
 library:ci-menhir:
   extends: .ci-template-flambda
 
+library:ci-interval:
+  extends: .ci-template-flambda
+  stage: stage-3
+  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-corn:
   extends: .ci-template-flambda
   stage: stage-4
diff --git a/Makefile.ci b/Makefile.ci
index 759462f509..d95ffa53e8 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -37,6 +37,7 @@ CI_TARGETS= \
     ci-geocoq \
     ci-coqhammer \
     ci-hott \
+    ci-interval \
     ci-iris \
     ci-math_classes \
     ci-mathcomp \
@@ -79,6 +80,8 @@ 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-simple_io: ci-ext_lib
 ci-quickchick: ci-ext_lib ci-simple_io
 
diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh
new file mode 100755
index 0000000000..30d437363f
--- /dev/null
+++ b/dev/ci/ci-interval.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download interval
+
+( cd "${CI_BUILD_DIR}/interval" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )