22 files changed, 144 insertions, 51 deletions
diff --git a/dev/base_include b/dev/base_include
index 1f14fc2941..daee2d97c5 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,7 +29,6 @@
 #install_printer ppatom;;
 #install_printer ppwhd;;
 #install_printer ppvblock;;
-#install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
 #install_printer  (* substitution *) ppsubst;;
 
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml
index a2207081f4..4275e3d121 100644
--- a/dev/bench/gitlab-bench.yml
+++ b/dev/bench/gitlab-bench.yml
@@ -28,5 +28,10 @@ bench:
     paths:
       - _bench/html/**/*.v.html
       - _bench/logs
+      - _bench/files.listing
+      - _bench/opam.NEW/**/*.log
+      - _bench/opam.NEW/**/*.timing
+      - _bench/opam.OLD/**/*.log
+      - _bench/opam.OLD/**/*.timing
     when: always
     expire_in: 1 year
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index 38b4e25bde..7625e4e7f7 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -12,6 +12,9 @@ r='\033[0m'          # reset (all attributes off)
 b='\033[1m'          # bold
 u='\033[4m'          # underline
 nl=$'\n'
+bt='`'               # backtick
+start_code_block='```'
+end_code_block='```'
 
 number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l)
 
@@ -36,6 +39,7 @@ echo $PWD
 #check_variable "BUILD_URL"
 #check_variable "JOB_NAME"
 #check_variable "JENKINS_URL"
+check_variable "CI_JOB_URL"
 check_variable "coq_pr_number"
 check_variable "coq_pr_comment_id"
 check_variable "new_ocaml_switch"
@@ -61,8 +65,9 @@ else
     exit 1
 fi
 
-mkdir -p "_bench"
-working_dir="$PWD/_bench"
+bench_dirname="_bench"
+mkdir -p "${bench_dirname}"
+working_dir="$PWD/${bench_dirname}"
 
 log_dir=$working_dir/logs
 mkdir "$log_dir"
@@ -109,6 +114,15 @@ else
     exit 1
 fi
 
+if which du > /dev/null; then
+    :
+else
+    echo > /dev/stderr
+    echo "ERROR: \"du\" program is not available." > /dev/stderr
+    echo > /dev/stderr
+    exit 1
+fi
+
 if [ ! -e "$working_dir" ]; then
     echo > /dev/stderr
     echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr
@@ -146,22 +160,31 @@ function coqbot_update_comment() {
 
     if [ ! -z "${coq_pr_number}" ]; then
         comment_text=""
+        artifact_text=""
 
         if [ -z "${is_done}" ]; then
             comment_text="in progress, "
+            artifact_text="eventually "
         else
             comment_text=""
+            artifact_text=""
         fi
-        comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})"
+        comment_text="Benchmarking ${comment_text}log available [here](${CI_JOB_URL}) ([raw log here](${CI_JOB_URL}/raw)), artifacts ${artifact_text}available for [download](${CI_JOB_URL}/artifacts/download) and [browsing](${CI_JOB_URL}/artifacts/browse)"
 
         if [ ! -z "${comment_body}" ]; then
-            comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```'
+            comment_text="${comment_text}${nl}${start_code_block}${nl}${comment_body}${nl}${end_code_block}"
         fi
 
         if [ ! -z "${uninstallable_packages}" ]; then
             comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}"
         fi
 
+        comment_text="${comment_text}${nl}${nl}<details><summary>Old Coq version ${old_coq_commit}</summary>"
+        comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}</details>"
+        comment_text="${comment_text}${nl}${nl}<details><summary>New Coq version ${new_coq_commit}</summary>"
+        comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}</details>"
+        comment_text="${comment_text}${nl}${nl}[Diff: ${bt}${old_coq_commit}..${new_coq_commit}${bt}](https://github.com/coq/coq/compare/${old_coq_commit}..${new_coq_commit})"
+
         # if there's a comment id, we update the comment while we're
         # in progress; otherwise, we wait until the end to post a new
         # comment
@@ -416,6 +439,11 @@ for coq_opam_package in $sorted_coq_opam_packages; do
     done
 done
 
+# Since we do not upload all files, store a list of the files
+# available so that if we at some point want to tweak which files we
+# upload, we'll know which ones are available for upload
+du -ha "$working_dir" > "$working_dir/files.listing"
+
 # The following directories in $working_dir are no longer used:
 #
 # - coq, opam.OLD, opam.NEW
@@ -430,7 +458,7 @@ done
 #
 # The next script processes all these files and prints results in a table.
 
-echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID"
+echo "INFO: workspace = ${CI_JOB_URL}/artifacts/browse/${bench_dirname}"
 
 # Print the final results.
 if [ -z "$installable_coq_opam_packages" ]; then
@@ -444,7 +472,7 @@ else
     rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)"
     echo "${rendered_results}"
 
-    echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/"
+    echo "INFO: per line timing: ${CI_JOB_URL}/artifacts/browse/${bench_dirname}/html/"
 
     cd "$coq_dir"
     echo INFO: Old Coq version
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index fd6ea9bb09..8eff2cf577 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -389,6 +389,7 @@ IF "%RUNSETUP%"=="Y" (
     -P libfontconfig1 ^
     -P gtk-update-icon-cache ^
     -P libtool,automake ^
+    -P libgmp-devel ^
     -P intltool ^
     -P bison,flex ^
     %EXTRAPACKAGES% ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index cc9fd13fdc..cde1d798a0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1006,6 +1006,7 @@ function make_ocaml_tools {
 
 function make_ocaml_libs {
   make_num
+  make_zarith
   make_findlib
   make_lablgtk
 }
@@ -1023,6 +1024,16 @@ function make_num {
   fi
 }
 
+function make_zarith {
+  make_ocaml
+  if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then
+    logn configure ./configure
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
 ##### OCAMLBUILD #####
 
 function make_ocamlbuild {
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 64936cd236..17d71ac52a 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -10,4 +10,4 @@ bash opam64/install.sh
 
 opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing
 eval "$(opam env)"
-opam install -y num ocamlfind dune ounit
+opam install -y num ocamlfind dune ounit zarith
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 2725e6b56c..75d9efaadc 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -62,9 +62,17 @@
 : "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
 : "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
 
-: "${lambda_rust_CI_REF:=master}"
-: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
-: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}"
+: "${autosubst_CI_REF:=coq86-devel}"
+: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}"
+: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}"
+
+: "${iris_string_ident_CI_REF:=master}"
+: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}"
+: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}"
+
+: "${iris_examples_CI_REF:=master}"
+: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}"
+: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh
new file mode 100755
index 0000000000..0256906112
--- /dev/null
+++ b/dev/ci/ci-iris.sh
@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+# Setup iris_examples and separate dependencies first
+git_download autosubst
+git_download iris_string_ident
+git_download iris_examples
+
+# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
+iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+
+# Setup Iris
+git_download iris
+
+# Extract required version of std++
+stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+
+# Setup std++
+git_download stdpp
+
+# Build std++
+( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
+
+# Build and validate Iris
+( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
+
+# Build autosubst
+( cd "${CI_BUILD_DIR}/autosubst" && make && make install )
+
+# Build iris-string-ident
+( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install )
+
+# Build Iris examples
+( cd "${CI_BUILD_DIR}/iris_examples" && make && make install )
diff --git a/dev/ci/ci-lambda_rust.sh b/dev/ci/ci-lambda_rust.sh
deleted file mode 100755
index 1ef0c2cb8f..0000000000
--- a/dev/ci/ci-lambda_rust.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-install_ssreflect
-
-# Setup lambda_rust first
-git_download lambda_rust
-
-# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
-
-# Setup Iris
-git_download iris
-
-# Extract required version of std++
-stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
-
-# Setup std++
-git_download stdpp
-
-# Build std++
-( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
-
-# Build and validate Iris
-( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
-
-# Build lambda_rust
-( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 67a8415891..78c8673299 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-08-18-V29"
+# CACHEKEY: "bionic_coq-V2020-08-28-V92"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -6,9 +6,14 @@ LABEL maintainer="e@x80.org"
 
 ENV DEBIAN_FRONTEND="noninteractive"
 
+# We need libgmp-dev:i386 for zarith; maybe we could also install GTK
+RUN dpkg --add-architecture i386
+
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
+        # Dependencies of ZArith
+        perl libgmp-dev libgmp-dev:i386 \
         # Dependencies of lablgtk (for CoqIDE)
         libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
@@ -35,10 +40,10 @@ ENV NJOBS="2" \
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.05.0"
 
-# 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.1 ounit2.2.2.3 odoc.1.5.0" \
+# Common OPAM packages, num to be removed once the migration to
+# micromega is complete, `num` also does not have a version number as
+# the right version to install varies with the compiler version.
+ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.11.0"
 
@@ -52,9 +57,10 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
     opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM
 
-# base+32bit switch
+# base+32bit switch, note the zarith hack
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install $BASE_OPAM
+        i386 env CC='gcc -m32' opam install zarith.1.9.1 && \
+        opam install $BASE_OPAM
 
 # EDGE switch
 ENV COMPILER_EDGE="4.10.0" \
diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
new file mode 100644
index 0000000000..da1d30c1e9
--- /dev/null
+++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then
+
+    bignums_CI_REF=zarith
+    bignums_CI_GITURL=https://github.com/ejgallego/bignums
+
+fi
diff --git a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
new file mode 100644
index 0000000000..bb08c13ef3
--- /dev/null
+++ b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then
+
+    elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
new file mode 100644
index 0000000000..f0878202d3
--- /dev/null
+++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then
+
+    elpi_CI_REF=update-s-univs
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=update-s-univs
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
new file mode 100644
index 0000000000..ee75944a52
--- /dev/null
+++ b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then
+
+    equations_CI_REF=delay-frozen-evarconv
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/dev/core.dbg b/dev/core.dbg
index ec946e2df0..6d52bae773 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,5 +1,6 @@
 load_printer threads.cma
 load_printer str.cma
+load_printer zarith.cma
 load_printer config.cma
 load_printer clib.cma
 load_printer dynlink.cma
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index 4e1035f7b6..3f73cf126a 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -1,5 +1,6 @@
 load_printer threads.cma
 load_printer str.cma
+load_printer zarith.cma
 load_printer config.cma
 load_printer clib.cma
 load_printer dynlink.cma
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index 3bf13da62d..5f826fe383 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -1,5 +1,6 @@
 load_printer threads.cma
 load_printer str.cma
+load_printer zarith.cma
 load_printer config.cma
 load_printer clib.cma
 load_printer dynlink.cma
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index 1267fd5393..2e58272c75 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -1,5 +1,6 @@
 load_printer threads.cma
 load_printer str.cma
+load_printer zarith.cma
 load_printer config.cma
 load_printer clib.cma
 load_printer lib.cma
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index a11269e059..91cb6168e1 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -34,4 +34,5 @@ exec $OCAMLDEBUG \
     -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
     -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
     -I $COQTOP/ide \
+    $(ocamlfind query -recursive -i-format zarith) \
     "$@"
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 63071bba72..60618f6491 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -23,7 +23,6 @@ install_printer Top_printers.ppconstr_expr
 install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
 install_printer Top_printers.ppnumtokunsigned
 install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ea90e83a83..773170207e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,7 +80,6 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
-let ppbigint n = pp (str (Bigint.to_string n));;
 let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
 let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 65eab8daa3..b1bb5e4702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -53,7 +53,6 @@ val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
 val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
 
-val ppbigint : Bigint.bigint -> unit
 val ppnumtokunsigned : NumTok.Unsigned.t -> unit
 val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit