5 files changed, 122 insertions, 25 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 95892ebe0a..3a179a9431 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -157,7 +157,7 @@ Currently available artifacts are:
   https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
 
   Additionally, an experimental Dune build is provided:
-  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev
 
 - the Coq documentation, built in the `doc:*` jobs. When submitting
   a documentation PR, this can help reviewers checking the rendered result:
@@ -167,7 +167,10 @@ 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
+    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
 
 ### GitLab and Windows
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 7a649591dd..b04161918e 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-08-27-V2"
+# CACHEKEY: "bionic_coq-V2018-09-23-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -7,50 +7,65 @@ LABEL maintainer="e@x80.org"
 ENV DEBIAN_FRONTEND="noninteractive"
 
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
-        m4 automake autoconf time wget rsync git gcc-multilib opam \
+        # Dependencies of the image, the test-suite and external projects
+        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
+        # Dependencies of lablgtk (for CoqIDE)
         libgtk2.0-dev libgtksourceview2.0-dev \
-        texlive-latex-extra texlive-fonts-recommended texlive-science tipa \
-        python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \
-        python3-setuptools python3-wheel python3-pip
+        # Dependencies of stdlib and sphinx doc
+        texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
+        xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
+        # Dependencies of source-doc and coq-makefile
+        texlive-science tipa
 
-RUN pip3 install antlr4-python3-runtime
+# More dependencies of the sphinx doc
+RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
+                 antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
+
+# We need to install OPAM 2.0 manually for now.
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
+    OPAMJOBS="2" \
     OPAMROOT=/root/.opamcache \
-    OPAMROOTISOK="true"
+    OPAMROOTISOK="true" \
+    OPAMYES="true"
 
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.02.3"
 
-RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
-
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \
     CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV CAMLP5_VER="6.14" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
-RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3
+RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
+    opam install ocamlfind.1.8.0 && \
+    opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
-RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
+RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
+    opam install ocamlfind.1.8.0 && \
+    opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
-    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
+    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
+    BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0"
 
-RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
+RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
+    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
-RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
+    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+
+RUN opam clean -a -c
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 973319de68..31bd65af08 100644..100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -2,6 +2,16 @@
 
 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:\cygwin*
+ECHO "Currently used target folders"
+DIR C:\coq*
+
 if %ARCH% == 32 (
   SET ARCHLONG=i686
   SET CYGROOT=C:\cygwin
@@ -14,11 +24,15 @@ if %ARCH% == 64 (
   SET SETUP=setup-x86_64.exe
 )
 
+SET DESTCOQ=C:\coq%ARCH%_inst
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
 powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
 SET CYGCACHE=%CYGROOT%\var\cache\setup
 SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
 SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
-SET DESTCOQ=C:\coq%ARCH%_inst
 SET COQREGTESTING=Y
 SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
 
@@ -29,10 +43,24 @@ 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% ^
   -addon="bignums ltac2 equations" -make=N ^
-  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
 
-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
+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 (
@@ -43,8 +71,49 @@ IF DEFINED WIN_CERTIFICATE_PATH (
   )
 )
 
+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%"
+  DEL /S /F /Q "%CYGROOT%" > NUL
+  ECHO "Cleaning %DESTCOQ%"
+  DEL /S /F /Q "%DESTCOQ%" > NUL
+  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/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
new file mode 100644
index 0000000000..019cb8054d
--- /dev/null
+++ b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then
+    cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification
+    cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto
+fi
diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
new file mode 100644
index 0000000000..3a6480a5a1
--- /dev/null
+++ b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then
+
+    ltac2_CI_BRANCH=master+globenv-coq-pr7288
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
+
+fi