aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-argosy.sh9
-rwxr-xr-xdev/ci/ci-basic-overlay.sh24
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
-rw-r--r--dev/ci/ci-common.sh16
-rwxr-xr-xdev/ci/ci-coquelicot.sh4
-rwxr-xr-xdev/ci/ci-unimath.sh4
-rwxr-xr-xdev/ci/gitlab.bat2
-rw-r--r--dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh18
-rw-r--r--dev/ci/user-overlays/08829-proj-syntax-check.sh5
-rw-r--r--dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh12
-rw-r--r--dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh30
-rw-r--r--dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh9
-rw-r--r--dev/ci/user-overlays/09733-gares-quotations.sh6
-rw-r--r--dev/ci/user-overlays/09815-token-type.sh4
-rw-r--r--dev/ci/user-overlays/09870-vbgl-recordops.sh6
-rw-r--r--dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh21
16 files changed, 147 insertions, 25 deletions
diff --git a/dev/ci/ci-argosy.sh b/dev/ci/ci-argosy.sh
new file mode 100755
index 0000000000..6137526bf4
--- /dev/null
+++ b/dev/ci/ci-argosy.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+FORCE_GIT=1
+git_download argosy
+
+( cd "${CI_BUILD_DIR}/argosy" && git submodule update --init --recursive && make )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index deeec3942d..0c89809ee9 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -24,9 +24,9 @@
########################################################################
# UniMath
########################################################################
-: "${UniMath_CI_REF:=master}"
-: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}"
-: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}"
+: "${unimath_CI_REF:=master}"
+: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}"
+: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}"
########################################################################
# Unicoq + Mtac2
@@ -104,15 +104,8 @@
########################################################################
# Coquelicot
########################################################################
-# The URL for downloading a tgz snapshot of the master branch is
-# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz
-# See https://gforge.inria.fr/scm/browser.php?group_id=3599
-# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently,
-# we use a fixed version, which has a download path which does fit to our standard mechanism.
-# ATTENTION: The archive URL might depend on the version!
-: "${Coquelicot_CI_REF:=coquelicot-3.0.2}"
-: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
-: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}"
+: "${coquelicot_CI_REF:=master}"
+: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
########################################################################
# CompCert
@@ -296,3 +289,10 @@
: "${stdlib2_CI_REF:=master}"
: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
+
+########################################################################
+# argosy
+########################################################################
+: "${argosy_CI_REF:=master}"
+: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}"
+: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2d242d80a4..2ac78d3c2b 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download bedrock2
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b4d2a9ca4e..7aa265cf90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -108,10 +108,9 @@ install_ssreflect()
git_download mathcomp
- ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
- make Makefile.coq && \
- make -f Makefile.coq ssreflect/all_ssreflect.vo && \
- make -f Makefile.coq install )
+ ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \
+ make && \
+ make install )
}
@@ -123,8 +122,11 @@ install_ssralg()
git_download mathcomp
( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
- make Makefile.coq && \
- make -f Makefile.coq algebra/all_algebra.vo && \
- make -f Makefile.coq install )
+ make -C ssreflect && \
+ make -C ssreflect install && \
+ make -C fingroup && \
+ make -C fingroup install && \
+ make -C algebra && \
+ make -C algebra install )
}
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 5d8817491d..33627fd8ef 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -6,6 +6,6 @@ ci_dir="$(dirname "$0")"
install_ssreflect
FORCE_GIT=1
-git_download Coquelicot
+git_download coquelicot
-( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index a7644fee23..704e278a4b 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -3,6 +3,6 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-git_download UniMath
+git_download unimath
-( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no )
+( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 5f819f31f9..cc1931d13d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,9 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
-addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot ^
-addon=vst ^
-addon=aactactics
+REM -addon=coquelicot ^
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
new file mode 100644
index 0000000000..67f6f8610a
--- /dev/null
+++ b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then
+
+ ltac2_CI_REF=master-parsing-decimal
+ ltac2_CI_GITURL=https://github.com/proux01/ltac2
+
+ quickchick_CI_REF=master-parsing-decimal
+ quickchick_CI_GITURL=https://github.com/proux01/QuickChick
+
+ Corn_CI_REF=master-parsing-decimal
+ Corn_CI_GITURL=https://github.com/proux01/corn
+
+ HoTT_CI_REF=master-parsing-decimal
+ HoTT_CI_GITURL=https://github.com/proux01/HoTT
+
+ stdlib2_CI_REF=master-parsing-decimal
+ stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+fi
diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh
new file mode 100644
index 0000000000..c04621114f
--- /dev/null
+++ b/dev/ci/user-overlays/08829-proj-syntax-check.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then
+ lambdaRust_CI_REF=proj-syntax-check
+ lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust
+ lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive
+fi
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
new file mode 100644
index 0000000000..12be1b676a
--- /dev/null
+++ b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
+
+ HoTT_CI_REF=rm-hardwired-hint-db
+ HoTT_CI_GITURL=https://github.com/vbgl/HoTT
+
+ ltac2_CI_REF=rm-hardwired-hint-db
+ ltac2_CI_GITURL=https://github.com/vbgl/ltac2
+
+ UniMath_CI_REF=rm-hardwired-hint-db
+ UniMath_CI_GITURL=https://github.com/vbgl/UniMath
+
+fi
diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh
new file mode 100644
index 0000000000..c09d1b8929
--- /dev/null
+++ b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh
@@ -0,0 +1,30 @@
+if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then
+
+ aac_tactics_CI_REF=proof+no_global_partial
+ aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+ # coqhammer_CI_REF=proof+no_global_partial
+ # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+ elpi_CI_REF=proof+no_global_partial
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ equations_CI_REF=proof+no_global_partial
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ ltac2_CI_REF=proof+no_global_partial
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ # unicoq_CI_REF=proof+no_global_partial
+ # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq
+
+ mtac2_CI_REF=proof+no_global_partial
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+ paramcoq_CI_REF=proof+no_global_partial
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+ quickchick_CI_REF=proof+no_global_partial
+ quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
new file mode 100644
index 0000000000..1e1d36d54a
--- /dev/null
+++ b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then
+
+ elpi_CI_REF=recarg-cleanup
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ quickchick_CI_REF=recarg-cleanup
+ quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh
new file mode 100644
index 0000000000..b17454fc4c
--- /dev/null
+++ b/dev/ci/user-overlays/09733-gares-quotations.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then
+
+ ltac2_CI_REF=quotations
+ ltac2_CI_GITURL=https://github.com/gares/ltac2
+
+fi
diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh
new file mode 100644
index 0000000000..4b49011de3
--- /dev/null
+++ b/dev/ci/user-overlays/09815-token-type.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then
+ ltac2_CI_REF=token-type
+ ltac2_CI_GITURL=https://github.com/proux01/ltac2
+fi
diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh
new file mode 100644
index 0000000000..bb14a8c204
--- /dev/null
+++ b/dev/ci/user-overlays/09870-vbgl-recordops.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then
+
+ elpi_CI_REF=pr-9870
+ elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
new file mode 100644
index 0000000000..01d3068591
--- /dev/null
+++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then
+
+ elpi_CI_REF=pretyping-rm-global
+ elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+ coqhammer_CI_REF=pretyping-rm-global
+ coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+ equations_CI_REF=pretyping-rm-global
+ equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+ ltac2_CI_REF=pretyping-rm-global
+ ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ paramcoq_CI_REF=pretyping-rm-global
+ paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+ mtac2_CI_REF=pretyping-rm-global
+ mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:55:53 +0000