aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/appveyor.bat1
-rw-r--r--dev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-elpi.sh10
-rw-r--r--dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh7
-rw-r--r--dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh6
-rw-r--r--dev/ci/user-overlays/06745-ejgallego-located+vernac.sh13
-rw-r--r--dev/ci/user-overlays/06775-univ-cumul-weak.sh4
-rw-r--r--dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh14
-rw-r--r--dev/ci/user-overlays/06837-ejgallego-located+libnames.sh15
-rw-r--r--dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh12
-rw-r--r--dev/ci/user-overlays/06923-ppedrot-export-options.sh7
11 files changed, 95 insertions, 0 deletions
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index dec6f0d182..85a71baf7f 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -23,6 +23,7 @@ if %USEOPAM% == false (
call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon=bignums -make=N ^
-setup %CYGROOT%\%SETUP% || GOTO ErrorExit
copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 784da6f971..48e01e9e93 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -144,3 +144,9 @@
########################################################################
: "${Equations_CI_BRANCH:=8.8+alpha}"
: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
+
+########################################################################
+# Elpi
+########################################################################
+: "${Elpi_CI_BRANCH:=coq-master}"
+: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}"
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
new file mode 100755
index 0000000000..c44e0a6552
--- /dev/null
+++ b/dev/ci/ci-elpi.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Elpi_CI_DIR=${CI_BUILD_DIR}/elpi
+
+git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR}
+
+( cd ${Elpi_CI_DIR} && make && make install )
diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
new file mode 100644
index 0000000000..4b681909d6
--- /dev/null
+++ b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
@@ -0,0 +1,7 @@
+ if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
+ ltac2_CI_BRANCH=econstr+more_fix
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=econstr+more_fix
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
new file mode 100644
index 0000000000..2451657d43
--- /dev/null
+++ b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then
+ ltac2_CI_BRANCH=fix-for/6676
+ ltac2_CI_GITURL=https://github.com/gares/ltac2.git
+ Equations_CI_BRANCH=fix-for/6676
+ Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
+fi
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
new file mode 100644
index 0000000000..d1d61fec2e
--- /dev/null
+++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
@@ -0,0 +1,13 @@
+if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then
+ ltac2_CI_BRANCH=located+vernac
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=located+vernac
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ fiat_parsers_CI_BRANCH=located+vernac
+ fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+ Elpi_CI_BRANCH=located+vernac
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+fi
diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
new file mode 100644
index 0000000000..8afcbf78a3
--- /dev/null
+++ b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then
+ Elpi_CI_BRANCH=coq-master
+ Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
+fi
diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
new file mode 100644
index 0000000000..df3e9cef28
--- /dev/null
+++ b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then
+
+ ltac2_CI_BRANCH=located+vernac_2
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=located+vernac_2
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ # fiat_parsers_CI_BRANCH=located+vernac
+ # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+ Elpi_CI_BRANCH=located+vernac_2
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+fi
diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
new file mode 100644
index 0000000000..a785290e7c
--- /dev/null
+++ b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then
+
+ ltac2_CI_BRANCH=located+libnames
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=located+libnames
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ Elpi_CI_BRANCH=located+libnames
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+ coq_dpdgraph_CI_BRANCH=located+libnames
+ coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git
+
+fi
diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
new file mode 100644
index 0000000000..5dedca0ca5
--- /dev/null
+++ b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then
+
+ Equations_CI_BRANCH=ssr+correct_packing
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ ltac2_CI_BRANCH=ssr+correct_packing
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Elpi_CI_BRANCH=ssr+correct_packing
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
new file mode 100644
index 0000000000..333a9e84bd
--- /dev/null
+++ b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then
+ ltac2_CI_BRANCH=export-options
+ ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+ Equations_CI_BRANCH=export-options
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:49:53 +0000