aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README.md12
-rwxr-xr-xdev/ci/ci-aac-tactics.sh8
-rwxr-xr-xdev/ci/ci-basic-overlay.sh11
-rwxr-xr-xdev/ci/ci-fiat-crypto-legacy.sh1
-rwxr-xr-xdev/ci/ci-iris-lambda-rust.sh4
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
-rwxr-xr-xdev/ci/gitlab.bat29
-rw-r--r--dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh11
-rw-r--r--dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh9
9 files changed, 62 insertions, 27 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 3a179a9431..7853866f62 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
developer who merges the PR on Coq. There are plans to improve this, cf.
[#6724](https://github.com/coq/coq/issues/6724).
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
Advanced GitLab CI information
------------------------------
@@ -167,10 +167,7 @@ Currently available artifacts are:
+ Coq's Standard Library Documentation [master branch]
https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman
+ Coq's ML API Documentation [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc
-
- The dune job also provides its own API documentation using the newer `odoc` tool:
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+ https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
### GitLab and Windows
@@ -178,6 +175,11 @@ If your repository has access to runners tagged `windows`, setting the
secret variable `WINDOWS` to `enabled` will add jobs building Windows
versions of Coq (32bit and 64bit).
+If the secret variable `WINDOWS` is set to `enabled_all_addons`,
+an extended set of addons will be added to the Windows installer.
+This leads to a considerable runtime in CI so this is not enabled
+by default for pipelines for pull requests.
+
The Windows jobs are enabled on Coq's repository, where pipelines for
pull requests run.
diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh
new file mode 100755
index 0000000000..896a0ddf66
--- /dev/null
+++ b/dev/ci/ci-aac-tactics.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download aactactics
+
+( cd "${CI_BUILD_DIR}/aactactics" && make && make install )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1b1aeafa0d..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -49,11 +49,12 @@
########################################################################
# Iris
########################################################################
-: "${stdpp_CI_REF:=master}"
+
+# NB: stdpp and Iris refs are gotten from the opam files in the Iris
+# and lambdaRust repos respectively.
: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
-: "${Iris_CI_REF:=master}"
: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
@@ -251,6 +252,6 @@
########################################################################
# aac-tactics
########################################################################
-: "${aactactis_CI_REF:=master}"
-: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
-: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
+: "${aactactics_CI_REF:=master}"
+: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index e0395754e5..6bf3138346 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -10,4 +10,5 @@ fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-d
fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+ ./etc/ci/remove_autogenerated.sh && \
make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index 6960a8b98a..95f143bb95 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,13 +9,13 @@ install_ssreflect
git_download lambdaRust
# Extract required version of Iris
-Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
# Setup Iris
git_download Iris
# Extract required version of std++
-stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
# Setup std++
git_download stdpp
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index fcfa591ce1..f257c62dd3 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-25-V1"
+# CACHEKEY: "bionic_coq-V2018-10-04-V2"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \
CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="7.01" \
+ENV CAMLP5_VER="7.03" \
COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
# base switch
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index deda42e2b7..918d289ae2 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -37,8 +37,21 @@ SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
SET COQREGTESTING=Y
SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+IF "%WINDOWS%" == "enabled_all_addons" (
+ SET EXTRA_ADDONS=^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot
+ REM addons with build issues
+ REM -addon=vst ^
+ REM -addon=aactactics ^
+) ELSE (
+ SET "EXTRA_ADDONS= "
+)
call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
@@ -47,20 +60,10 @@ call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-addon=equations ^
-addon=ltac2 ^
-addon=mtac2 ^
- -addon=mathcomp ^
- -addon=menhir ^
- -addon=menhirlib ^
- -addon=compcert ^
- -addon=extlib ^
- -addon=quickchick ^
- -addon=coquelicot ^
+ %EXTRA_ADDONS% ^
-make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-REM addons with build issues
-REM -addon=vst ^
-REM -addon=aactactics ^
-
ECHO "Start Artifact Creation"
TIME /T
diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
new file mode 100644
index 0000000000..484ad8f9e6
--- /dev/null
+++ b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
@@ -0,0 +1,11 @@
+if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then
+
+ ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env
+ ltac2_CI_REF=master+fix-pr8554-change-takes-env
+ ltac2_CI_GITURL=https://github.com/herbelin/ltac2
+
+ Equations_CI_BRANCH=master+fix-pr8554-change-takes-env
+ Equations_CI_REF=master+fix-pr8554-change-takes-env
+ Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
new file mode 100644
index 0000000000..41c2ad6fef
--- /dev/null
+++ b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then
+
+ ltac2_CI_REF=rm-section-path
+ ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ Equations_CI_REF=rm-section-path
+ Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:05:07 +0000