14 files changed, 154 insertions, 159 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 97d9537508..8bcbd90f0b 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -101,7 +101,7 @@ project geocoq "https://github.com/GeoCoq/GeoCoq" "master"
 ########################################################################
 # Flocq
 ########################################################################
-project flocq "https://gitlab.inria.fr/flocq/flocq" "master"
+project flocq "https://gitlab.inria.fr/flocq/flocq" "flocq-3"
 
 ########################################################################
 # coq-performance-tests
diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh
index fde8df8e3d..2fa4d5c776 100755
--- a/dev/ci/ci-coq_performance_tests.sh
+++ b/dev/ci/ci-coq_performance_tests.sh
@@ -5,4 +5,9 @@ ci_dir="$(dirname "$0")"
 
 git_download coq_performance_tests
 
-( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf-Sanity && make validate && make install )
+# run make -k; make again if make fails so that the failing file comes last, so that it's easier to find the error messages in the CI log
+function make_full() {
+    if ! make -k "$@"; then make -k "$@"; exit 1; fi
+}
+
+( cd "${CI_BUILD_DIR}/coq_performance_tests" && make_full coq perf-Sanity && make validate && make install )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 16c4ac37d9..ed51c8afd3 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -4,31 +4,29 @@ This directory provides Docker images to be used by Coq's CI. The
 images do support Docker autobuild on `hub.docker.com` and Gitlab's
 private registry.
 
-The Gitlab CI will build a docker image unless the CI environment variable
+The Gitlab CI will build a Docker image unless the CI environment variable
 `SKIP_DOCKER` is set to `true`. This image will be
 stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry)
 under the name given by the `CACHEKEY` variable from
 the [Gitlab CI configuration file](../../../.gitlab-ci.yml).
 
-In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job.
+`SKIP_DOCKER` is set to "true" in `https://gitlab.com/coq/coq` to avoid running
+a lengthy redundant job.  For efficiency, users should enable that setting
+in forked repositories after the initial Docker build in the fork succeeds.
 
-It can be used to regenerate a fresh Docker image on Gitlab through the following steps.
-- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit.
-- Push this commit to a Github PR. This will trigger a Gitlab CI run that will
-  immediately fail, as the Docker image is missing and the `SKIP_DOCKER`
+The steps to generate a new Docker image are:
+- Update the `CACHEKEY` variable in .gitlab-ci.yml with the date and md5.
+- Submit the change in a PR. This triggers a Gitlab CI run that
+  immediately fails, as the Docker image is missing and the `SKIP_DOCKER`
   default value prevents rebuilding the image.
-- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline"
-  button on the [web interface](https://gitlab.com/coq/coq/pipelines),
-  with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and
-  once completed, a new Docker image will be available in the container registry,
-  with the name set in `CACHEKEY`.
+- Run a new pipeline on Gitlab with that PR branch (e.g. "pr-99999"), using the green
+  "Run pipeline" button on the [web interface](https://gitlab.com/coq/coq/pipelines),
+  with the `SKIP_DOCKER` environment variable set to `false`. This will run a
+  `docker-boot` process, and once completed, a new Docker image will be available in
+  the container registry, with the name set in `CACHEKEY`.
 - Any pipeline with the same `CACHEKEY` will now automatically reuse that
   image without rebuilding it from scratch.
 
-For documentation purposes, we also require keeping in sync the `CACHEKEY` comment
-from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same
-commit.
-
 In case you do not have the rights to run Gitlab CI pipelines, you should ask
 the ci-maintainers Github team to do it for you.
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 1aefebb007..8f14625c63 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -44,7 +44,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.12.0"
+    BASE_ONLY_OPAM="elpi.1.13.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
@@ -71,3 +71,6 @@ RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM
 
 RUN opam clean -a -c
+
+# set the locale for the benefit of Python
+ENV LANG C.UTF-8
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
deleted file mode 100755
index dc6423332f..0000000000
--- a/dev/ci/gitlab.bat
+++ /dev/null
@@ -1,141 +0,0 @@
-@ECHO OFF
-
-REM This script builds and signs the Windows packages on Gitlab
-
-ECHO "Start Time"
-TIME /T
-
-REM List currently used cygwin and target folders for debugging / maintenance purposes
-
-ECHO "Currently used cygwin folders"
-DIR C:\ci\cygwin*
-ECHO "Currently used target folders"
-DIR C:\ci\coq*
-ECHO "Root folders"
-DIR C:\
-
-if %ARCH% == 32 (
-  SET ARCHLONG=i686
-  SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
-  SET ARCHLONG=x86_64
-  SET SETUP=setup-x86_64.exe
-)
-
-SET CYGROOT=C:\ci\cygwin%ARCH%
-SET DESTCOQ=C:\ci\coq%ARCH%
-SET CYGCACHE=C:\ci\cache\cgwin
-
-CALL :MakeUniqueFolder %CYGROOT% CYGROOT
-CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
-
-powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
-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 "%WINDOWS%" == "enabled_all_addons" (
-  SET EXTRA_ADDONS=^
-    -addon=bignums ^
-    -addon=equations ^
-    -addon=mtac2 ^
-    -addon=mathcomp ^
-    -addon=menhir ^
-    -addon=menhirlib ^
-    -addon=compcert ^
-    -addon=extlib ^
-    -addon=quickchick ^
-    -addon=coquelicot ^
-    -addon=vst ^
-    -addon=aactactics ^
-    -addon=flocq ^
-    -addon=interval ^
-    -addon=gappa_tool ^
-    -addon=gappa ^
-    -addon=elpi ^
-    -addon=HB
-) 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% ^
-  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-  %EXTRA_ADDONS% ^
-  -make=N ^
-  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-
-ECHO "Start Artifact Creation"
-TIME /T
-
-mkdir artifacts
-
-CALL :CopyLogFiles
-
-copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
-REM The open source archive is only required for release builds
-IF DEFINED WIN_CERTIFICATE_PATH (
-  7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-) ELSE (
-  REM In non release builds, create a dummy file
-  ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
-)
-
-REM DO NOT echo the signing command below, as this would leak secrets in the logs
-IF DEFINED WIN_CERTIFICATE_PATH (
-  IF DEFINED WIN_CERTIFICATE_PASSWORD (
-    ECHO Signing package
-    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
-    signtool verify /pa dev\nsis\*.exe
-  )
-)
-
-ECHO "Finished Artifact Creation"
-TIME /T
-
-CALL :CleanupFolders
-
-ECHO "Finished Cleanup"
-TIME /T
-
-GOTO :EOF
-
-:CopyLogFiles
-  ECHO Copy log files for artifact upload
-  MKDIR artifacts\buildlogs
-  COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
-  MKDIR artifacts\filelists
-  COPY %CYGROOT%\build\filelists\* artifacts\filelists
-  MKDIR artifacts\flagfiles
-  COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
-  GOTO :EOF
-
-:CleanupFolders
-  ECHO "Cleaning %CYGROOT%"
-  RMDIR /S /Q "%CYGROOT%"
-  ECHO "Cleaning %DESTCOQ%"
-  RMDIR /S /Q "%DESTCOQ%"
-  GOTO :EOF
-
-:MakeUniqueFolder
-  REM Create a uniquely named folder
-  REM This script is safe because folder creation is atomic - either we create it or fail
-  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
-  REM %2 = name of the variable which receives the unique folder name
-  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
-  MKDIR "%UNIQUENAME%"
-  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
-  SET "%2=%UNIQUENAME%"
-  GOTO :EOF
-
-:ErrorCopyLogFilesAndExit
-  CALL :CopyLogFiles
-  REM fall through
-
-:ErrorExit
-  CALL :CleanupFolders
-  ECHO ERROR %0 failed
-  EXIT /b 1
diff --git a/dev/ci/platform-windows.bat b/dev/ci/platform-windows.bat
new file mode 100755
index 0000000000..513aec5f94
--- /dev/null
+++ b/dev/ci/platform-windows.bat
@@ -0,0 +1,105 @@
+REM @ECHO OFF
+
+REM SET ARCH=64
+REM SET PLATFORM=https://github.com/coq/platform/archive/v8.13.zip
+REM SET CI_PROJECT_DIR=C:\root
+
+REM This script builds a minimal Windows platform on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+ECHO "Powershell version"
+powershell -Command "Get-Host"
+ECHO "Git installation of Mingw"
+DIR "C:\Program Files\Git\mingw64\bin\*.exe"
+
+ECHO "--------- START -------"
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+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\Git\mingw64\bin
+
+
+ECHO "Downloading %PLATFORM%"
+curl -L -o platform.zip "%PLATFORM%"
+7z x platform.zip
+
+cd platform-*
+
+call coq_platform_make_windows.bat ^
+  -arch=%ARCH% ^
+  -destcyg=%CYGROOT% ^
+  -cygcache=%CYGCACHE% ^
+  -extent=i ^
+  -parallel=p ^
+  -jobs=2 ^
+  -switch=d || GOTO ErrorCopyLogFilesAndExit
+
+cd ..
+
+SET BASH=%CYGROOT%\bin\bash
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+MKDIR %CI_PROJECT_DIR%\artifacts
+%BASH% --login -c "cd coq-platform && windows/create_installer_windows.sh && cp windows_installer/*.exe %CI_PROJECT_DIR_CFMT%/artifacts" || GOTO ErrorCopyLogFilesAndExit
+TIME /T
+
+CALL :CopyLogFiles
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+  ECHO Copy log files for artifact upload
+  REM This is currently not supported by the opam based build scripts
+  GOTO :EOF
+
+:CleanupFolders
+  ECHO "Cleaning %CYGROOT%"
+  RMDIR /S /Q "%CYGROOT%"
+  GOTO :EOF
+
+:MakeUniqueFolder
+  REM Create a uniquely named folder
+  REM This script is safe because folder creation is atomic - either we create it or fail
+  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+  REM %2 = name of the variable which receives the unique folder name
+  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+  MKDIR "%UNIQUENAME%"
+  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+  RMDIR "%UNIQUENAME%"
+  SET "%2=%UNIQUENAME%"
+  GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+  CALL :CopyLogFiles
+  REM fall through
+
+:ErrorExit
+  CALL :CleanupFolders
+  ECHO ERROR %0 failed
+  EXIT /b 1
diff --git a/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh
new file mode 100644
index 0000000000..dc57e6efb9
--- /dev/null
+++ b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh
@@ -0,0 +1,9 @@
+overlay coq_dpdgraph https://github.com/ppedrot/coq-dpdgraph compact-case-repr 13563
+overlay coqhammer https://github.com/ppedrot/coqhammer compact-case-repr 13563
+overlay elpi https://github.com/ppedrot/coq-elpi compact-case-repr 13563
+overlay equations https://github.com/ppedrot/Coq-Equations compact-case-repr 13563
+overlay metacoq https://github.com/ppedrot/metacoq compact-case-repr 13563
+overlay mtac2 https://github.com/ppedrot/Mtac2 compact-case-repr 13563
+overlay paramcoq https://github.com/ppedrot/paramcoq compact-case-repr 13563
+overlay relation_algebra https://github.com/ppedrot/relation-algebra compact-case-repr 13563
+overlay unicoq https://github.com/ppedrot/unicoq compact-case-repr 13563
diff --git a/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
new file mode 100644
index 0000000000..d80363c49f
--- /dev/null
+++ b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi debug-infra 13202
diff --git a/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh
new file mode 100644
index 0000000000..27e7cee42e
--- /dev/null
+++ b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13299" ] || [ "$CI_BRANCH" = "preserve-universes-notation" ]; then
+
+    elpi_CI_REF=overlay-universes-in-notations
+    elpi_CI_GITURL=https://github.com/jashug/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh b/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh
new file mode 100644
index 0000000000..0f62d0ee9f
--- /dev/null
+++ b/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh
@@ -0,0 +1 @@
+overlay equations https://github.com/ppedrot/Coq-Equations mv-evaluable-global-ref-out-of-kernel 13321
diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh
new file mode 100644
index 0000000000..4c8cdbbb45
--- /dev/null
+++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then
+
+    overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern
+
+fi
diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
new file mode 100644
index 0000000000..69bd038b78
--- /dev/null
+++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
@@ -0,0 +1 @@
+overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725
diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh
new file mode 100644
index 0000000000..d9a1736532
--- /dev/null
+++ b/dev/ci/user-overlays/13844-gares-command-loc.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844
diff --git a/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
new file mode 100644
index 0000000000..6847bde6d8
--- /dev/null
+++ b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.0 13847