9 files changed, 217 insertions, 21 deletions
diff --git a/dev/build/windows/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_master_installer.bat
index f4f5827328..72640d5d79 100755
--- a/dev/build/windows/MakeCoq_trunk_installer.bat
+++ b/dev/build/windows/MakeCoq_master_installer.bat
@@ -16,7 +16,7 @@ call MakeCoq_SetRootPath
 call MakeCoq_MinGW.bat ^
   -arch=64 ^
   -installer=Y ^
-  -coqver=git-trunk ^
+  -coqver=git-master ^
   -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^
   -destcoq="%ROOTPATH%\coq64_trunk_inst"
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 859b3e3166..963b0e6387 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -983,6 +983,15 @@ function make_ocaml {
       cp Changes      "$PREFIXOCAML/license_readme/ocaml/Changes.txt"
     fi
 
+    # Since 4.07 this library is part of ocaml
+    mkdir -p "$PREFIXOCAML/libocaml/site-lib/seq/"
+    cat > "$PREFIXOCAML/libocaml/site-lib/seq/META" <<EOT
+name="seq"
+version="[distributed with OCaml 4.07 or above]"
+description="dummy backward-compatibility package for iterators"
+requires=""
+EOT
+
     build_post
   fi
 }
@@ -1093,13 +1102,14 @@ function make_camlp5 {
   make_ocaml
   make_findlib
 
-  if build_prep https://github.com/camlp5/camlp5/archive rel707 tar.gz 1 camlp5-rel707; then
+  if build_prep https://github.com/camlp5/camlp5/archive rel711 tar.gz 1 camlp5-rel711; then
     logn configure ./configure
     # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
     sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
     # shellcheck disable=SC2086
     log1 make world.opt $MAKE_OPT
     log2 make install
+    cp lib/*.a "$PREFIXOCAML/libocaml/camlp5/"
     log2 make clean
     # For some reason META is not built / copied, but it is required
     log2 make -C etc META
@@ -1154,6 +1164,47 @@ function make_lablgtk {
   fi
 }
 
+##### Elpi #####
+
+function make_seq {
+  make_ocaml
+  # since 4.07 this package is part of ocaml
+
+}
+
+function make_re {
+  make_ocaml
+  make_dune
+  make_seq
+
+  if build_prep https://github.com/ocaml/ocaml-re/archive 1.9.0 tar.gz 1 ocaml-re; then
+
+    log2 dune build -p re
+    log2 dune install re
+
+    build_post
+  fi
+
+}
+
+function make_elpi {
+  make_ocaml
+  make_findlib
+  make_camlp5
+  make_dune
+  make_re
+
+  if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then
+
+    log2 make build DUNE_OPTS="-p elpi"
+    log2 make install DUNE_OPTS="-p elpi"
+
+    build_post
+
+  fi
+
+}
+
 ##### COQ #####
 
 # Copy one DLLfrom cygwin MINGW packages to Coq install folder
@@ -1904,6 +1955,36 @@ function make_addon_gappa {
   fi
 }
 
+# Elpi: extension language for Coq based. It lets one define commands in tactics
+# in a high level programming language with support for binders and unification
+# variables.
+
+function make_addon_elpi {
+  make_elpi
+  installer_addon_dependency elpi
+  if build_prep_overlay elpi ; then
+    installer_addon_section elpi "Elpi extension language" "Coq plugin for the Elpi extension language" ""
+    logn build make
+    logn installe make install
+    build_post
+  fi
+}
+
+# Hierarchy Builder: high level language to declare a hierarchy of structures
+# compiled down to records and canonical structures.
+
+function make_addon_HB {
+  installer_addon_dependency_beg elpi_hb
+  make_addon_elpi
+  installer_addon_dependency_end
+  if build_prep_overlay elpi_hb ; then
+    installer_addon_section elpi_hb "Hierarchy Builder" "Coq library to declare algebraic hierarchies" ""
+    logn build make
+    logn install make install VFILES=structures.v
+    build_post
+  fi
+}
+
 # Main function for building addons
 
 function make_addons {
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b87a9c0392..5f7d0b5789 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -351,3 +351,10 @@
 : "${metacoq_CI_REF:=master}"
 : "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
 : "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
+
+########################################################################
+# SF suite
+########################################################################
+: "${sf_CI_REF:=master}"
+: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
+: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index b9d6215e60..d46e53717f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,22 +3,9 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
+git_download sf
 
-# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
-# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-
-mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
-
-sf_lf_CI_TARURL=$(echo "$data"  | jq -rc '.[] | select (.path == "lf.tgz") | .url')
-sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url')
-sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url')
-
-wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-
-( cd lf  && make clean && make )
-( cd plf && make clean && make )
-( cd vfa && make clean && make )
+( cd lf-current  && make clean && make )
+( cd plf-current && make clean && make )
+( cd vfa-current && make clean && make )
+# ( cd qc-current && make clean && make )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 3998fc6514..dc6423332f 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -54,7 +54,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=flocq ^
     -addon=interval ^
     -addon=gappa_tool ^
-    -addon=gappa
+    -addon=gappa ^
+    -addon=elpi ^
+    -addon=HB
 ) ELSE (
   SET "EXTRA_ADDONS= "
 )
diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
new file mode 100644
index 0000000000..c9ddb3fb9f
--- /dev/null
+++ b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then
+
+    equations_CI_REF="rm-local-reductionops"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    unicoq_CI_REF="rm-local-reductionops"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
new file mode 100644
index 0000000000..0b3133d1f1
--- /dev/null
+++ b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11948" ] || [ "$CI_BRANCH" = "hexadecimal" ]; then
+
+    stdlib2_CI_REF=hexadecimal
+    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+    paramcoq_CI_REF=hexadecimal
+    paramcoq_CI_GITURL=https://github.com/proux01/paramcoq
+
+    metacoq_CI_REF=hexadecimal
+    metacoq_CI_GITURL=https://github.com/proux01/metacoq
+
+fi
diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
new file mode 100644
index 0000000000..50eaf0b109
--- /dev/null
+++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then
+
+    elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/tools/generate-release-changelog.sh b/dev/tools/generate-release-changelog.sh
new file mode 100755
index 0000000000..5b2d749b66
--- /dev/null
+++ b/dev/tools/generate-release-changelog.sh
@@ -0,0 +1,92 @@
+#!/usr/bin/env bash
+
+set -e
+set -o pipefail
+
+if [ $# != 1 ]; then
+    echo "Usage: $0 BRANCH"
+    exit
+fi
+
+branch=$1
+
+# Set SLOW_CONF to have the confirmation output wait for a newline
+# Emacs doesn't send characters until the RET so we can't quick_conf
+if [ -z ${SLOW_CONF+x} ] || [ -n "$INSIDE_EMACS" ]; then
+    quick_conf="-n 1"
+else
+    quick_conf=""
+fi
+
+ask_confirmation() {
+    read -p "Continue anyway? [y/N] " $quick_conf -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+}
+
+if ! git diff --quiet; then
+    echo "Warning: current tree is dirty."
+    ask_confirmation
+fi
+
+remote=$(git config --get "branch.${branch}.remote")
+
+if [ -z "$remote" ]; then
+    echo "Warning: branch $branch has no associated remote."
+    ask_confirmation
+else
+
+    if [ "$remote" != $(git config --get "branch.master.remote") ]; then
+        echo "Warning: branch master and branch $branch do not have the same remote."
+        ask_confirmation
+    fi
+
+    official_remote_git_url="git@github.com:coq/coq"
+    official_remote_https_url="github.com/coq/coq"
+    remote_url=$(git remote get-url "$remote" --all)
+
+    if [ "$remote_url" != "${official_remote_git_url}" ] && \
+           [ "$remote_url" != "${official_remote_git_url}.git" ] && \
+           [ "$remote_url" != "https://${official_remote_https_url}" ] && \
+           [ "$remote_url" != "https://${official_remote_https_url}.git" ] && \
+           [[ "$remote_url" != "https://"*"@${official_remote_https_url}" ]] && \
+           [[ "$remote_url" != "https://"*"@${official_remote_https_url}.git" ]] ; then
+        echo "Warning: remote $remote does not point to the official Coq repo,"
+        echo "that is $official_remote_git_url"
+        echo "It points to $remote_url instead."
+        ask_confirmation
+    fi
+
+    git fetch "$remote"
+
+    if [ $(git rev-parse master) != $(git rev-parse "${remote}/master") ]; then
+        echo "Warning: branch master is not up-to-date with ${remote}/master."
+        ask_confirmation
+    fi
+
+    if [ $(git rev-parse "$branch") != $(git rev-parse "${remote}/${branch}") ]; then
+        echo "Warning: branch ${branch} is not up-to-date with ${remote}/${branch}."
+        ask_confirmation
+    fi
+
+fi
+
+git checkout $branch --detach
+changelog_entries_with_title=$(ls doc/changelog/*/*.rst)
+changelog_entries_no_title=$(echo "$changelog_entries_with_title" | grep -v "00000-title.rst")
+git checkout master
+for f in $changelog_entries_with_title; do
+    if [ -f "$f" ]; then
+        cat "$f" >> released.rst
+    else
+        echo "Warning: $f is missing in master branch."
+    fi
+done
+for f in $changelog_entries_no_title; do
+    if [ -f "$f" ]; then
+        git rm "$f"
+    fi
+done
+echo "Changelog written in released.rst. Move its content to a new section in doc/sphinx/changes.rst."