Merge PR #9701: [CI] Add stdlib2

Reviewed-by: ejgallego

4 files changed, 19 insertions, 0 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index fd1ea325e9..c5038d3bb0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -584,6 +584,9 @@ library:ci-math-comp:
 library:ci-sf:
   <<: *ci-template
 
+library:ci-stdlib2:
+  <<: *ci-template-flambda
+
 library:ci-unimath:
   <<: *ci-template-flambda
 
diff --git a/Makefile.ci b/Makefile.ci
index 0307d39d54..9180d51bee 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -40,6 +40,7 @@ CI_TARGETS= \
     ci-relation-algebra \
     ci-sf \
     ci-simple-io \
+    ci-stdlib2 \
     ci-tlc \
     ci-unimath \
     ci-verdi-raft \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 74e8d3bbaa..deeec3942d 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -289,3 +289,10 @@
 : "${verdi_raft_CI_REF:=master}"
 : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
 : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
+
+########################################################################
+# stdlib2
+########################################################################
+: "${stdlib2_CI_REF:=master}"
+: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
+: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh
new file mode 100755
index 0000000000..ec1c180d7d
--- /dev/null
+++ b/dev/ci/ci-stdlib2.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download stdlib2
+
+( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install)