aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-perennial.sh5
-rw-r--r--dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh15
-rw-r--r--dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh6
-rw-r--r--dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh6
4 files changed, 28 insertions, 4 deletions
diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh
index f3be66e814..306cbdf63c 100755
--- a/dev/ci/ci-perennial.sh
+++ b/dev/ci/ci-perennial.sh
@@ -6,7 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download perennial
-# required by Perennial's coqc.py build wrapper
-export LC_ALL=C.UTF-8
-
-( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false )
+( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite )
diff --git a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
new file mode 100644
index 0000000000..1473f6df8b
--- /dev/null
+++ b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12653" ] || [ "$CI_BRANCH" = "cumul-syntax" ]; then
+
+ overlay elpi https://github.com/SkySkimmer/coq-elpi cumul-syntax
+
+ overlay equations https://github.com/SkySkimmer/Coq-Equations cumul-syntax
+
+ overlay mtac2 https://github.com/SkySkimmer/Mtac2 cumul-syntax
+
+ overlay paramcoq https://github.com/SkySkimmer/paramcoq cumul-syntax
+
+ overlay rewriter https://github.com/SkySkimmer/rewriter cumul-syntax
+
+ overlay metacoq https://github.com/SkySkimmer/metacoq cumul-syntax
+
+fi
diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
new file mode 100644
index 0000000000..7680e8da78
--- /dev/null
+++ b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then
+
+ equations_CI_REF=master+fix12873-better-unification
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh
new file mode 100644
index 0000000000..3bdbcf7d6e
--- /dev/null
+++ b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then
+
+ overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single
+ overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single
+
+fi