8 files changed, 233 insertions, 60 deletions
diff --git a/dev/base_include b/dev/base_include
index 1fb80dc07..e76044f41 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -232,7 +232,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
 
 let _ =
  print_string
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 8c8c0d8be..8e0d2341d 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -854,7 +854,7 @@ function make_ocaml_libs {
 
 function make_findlib {
   make_ocaml
-  if build_prep http://download.camlcity.org/download findlib-1.5.6 tar.gz 1 ; then
+  if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then
     logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
     # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
     log2 make all
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 4e8c7e145..4f7e9517f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -11,25 +11,6 @@ wget -qO- ${sf_vfa_CI_TARURL} | tar xvz
 sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
 sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
 
-# Delete useless calls to try omega; unfold
-patch vfa/SearchTree.v <<EOF
-*** SearchTree.v.bak	2017-09-06 19:12:59.000000000 +0200
---- SearchTree.v	2017-11-21 16:34:41.000000000 +0100
-***************
-*** 674,683 ****
-     forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j.
-  Proof.
-  intros.
-- try omega.  (* Oops! [omega] cannot solve this one.
--     The problem is that [i] and [j] have type [key] instead of type [nat].
--     The solution is easy enough: *)
-- unfold key in *.
-  omega.
-
-  (** So, if you get stuck on an [omega] that ought to work,
---- 674,679 ----
-EOF
-
 ( cd lf && make clean && make )
 
 ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index df366a978..3a2df6a81 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,6 +1,7 @@
 # Merging changes in Coq
 
-This document describes how patches (submitted as Pull Requests) should be
+This document describes how patches (submitted as pull requests
+on the `master` branch) should be
 merged into the main repository (https://github.com/coq/coq).
 
 ## Code owners
@@ -9,25 +10,29 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
 system, two owners. One is the principal maintainer of the component, the other
 is the secondary maintainer.
 
-When a pull request is submitted, GitHub will automatically ask these two
-maintainers for a review. If the pull request touches several parts, all the
-corresponding maintainers will be asked for a review.
+When a pull request is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the pull request touches several parts, all the
+corresponding principal maintainers will be asked for a review.
 
 Maintainers are never assigned as reviewer on their own PRs.
 
+If a principal maintainer submits a PR that changes the component they own, they
+must assign the secondary maintainer as reviewer. They should also do it if they
+know they are not available to do the review.
+
 ## Reviewing
 
-When principal maintainers receive a review request, they are expected to:
+When maintainers receive a review request, they are expected to:
 
 * Put their name in the assignee field, if they are in charge of the component
-  that is the main target of the patch (or if they are the only principal
-  maintainer asked to review the PR).
+  that is the main target of the patch (or if they are the only maintainer asked
+  to review the PR).
 * Review the PR, approve it or request changes.
 * If they are the assignee, check if all reviewers approved the PR. If not,
   regularly ping the author (if changes should be implemented) or the reviewers
   (if reviews are missing). The assignee ensures that any requests for more
-  discussion have been granted. When the discussion has converged and all
-  reviewers have approved the PR, the assignee is expected to follow the merging
+  discussion have been granted. When the discussion has converged and ALL
+  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
   process described below.
 
 In all cases, maintainers can delegate reviews to the other maintainer of the
@@ -37,6 +42,11 @@ patch.
 A maintainer is expected to be reasonably reactive, but no specific timeframe is
 given for reviewing.
 
+(*) In case a component is touched in a trivial way (adding/removing one file in
+a `Makefile`, etc), or by applying a systematic process (global renaming,
+deprecationg propagation, etc) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required and proceed with the merge.
+
 ## Merging
 
 Once all reviewers approved the PR, the assignee is expected to check that CI
@@ -45,10 +55,68 @@ documentation and test cases. If not, they should leave a comment on the PR and
 put the approriate label. Otherwise, they are expected to merge the PR using the
 [merge script](/dev/tools/merge-pr.sh).
 
-The command to be used is:
+When the PR has conflicts, the assignee can either:
+- ask the author to rebase the branch, fixing the conflicts
+- warn the author that they are going to rebase the branch, and push to the
+  branch directly
+
+In both cases, CI should be run again.
+
+In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+the conflicts in the merge commit (following the same steps as below), and push
+to `master` directly. Don't use the GitHub interface to fix these conflicts.
+
+To merge the PR proceed in the following way
 ```
+$ git checkout master
+$ git pull
 $ dev/tools/merge-pr XXXX
+$ git push upstream
 ```
-where `XXXX` is the number of the PR to be merged. This operation should be followed by a push.
+where `XXXX` is the number of the PR to be merged and `upstream` is the name
+of your remote pointing to `git@github.com:coq/coq.git`.
+Note that you are only supposed to merge PRs into `master`. PRs should rarely
+target the stable branch, but when it is the case they are the responsibility
+of the release manager.
+
+This script conducts various checks before proceeding to merge. Don't bypass them
+without a good reason to, and in that case, write a comment in the PR thread to
+explain the reason.
 
 Maintainers MUST NOT merge their own patches.
+
+DON'T USE the GitHub interface for merging, since it will prevent the automated
+backport script from operating properly, generates bad commit messages, and a
+messy history when there are conflicts.
+
+### What to do if the PR has overlays
+
+If the PR breaks compatibility of some developments in CI, then the author must
+have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md))
+and the PR must absolutely update the `CHANGES` file.
+
+There are two cases to consider:
+
+- If the patch is backward compatible (best scenario), then you should get
+  upstream maintainers to integrate it before merging the PR.
+- If the patch is not backward compatible (which is often the case when
+  patching plugins after an update to the Coq API), then you can proceed to
+  merge the PR and then notify upstream they can merge the patch. This is a
+  less preferable scenario because it is probably going to create
+  spurious CI failures for unrelated PRs.
+
+### Merge script dependencies
+
+The merge script passes option `-S` to `git merge` to ensure merge commits
+are signed. Consequently, it depends on the GnuPG command utility being
+installed and a GPG key being available. Here is a short tutorial to
+creating your own GPG key:
+<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/>
+
+The script depends on a few other utilities. If you are a Nix user, the
+simplest way of getting them is to run `nix-shell` first.
+
+**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG
+is not out of the box. Installing explicitly "pinentry-mac" seems important for
+typing of passphrase to work correctly (see also this
+[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)).
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index ee9c8777a..cd09b6d30 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -31,4 +31,6 @@ fi
 find . "(" -path ./.git -prune ")" -o -type f -print0 |
     xargs -0 dev/tools/check-eof-newline.sh || CODE=1
 
+dev/tools/check-overlays.sh || CODE=1
+
 exit $CODE
diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh
new file mode 100755
index 000000000..f7e05b51c
--- /dev/null
+++ b/dev/tools/check-overlays.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+for f in dev/ci/user-overlays/*
+do
+    if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]])
+    then
+        >&2 echo "Bad overlay '$f'."
+        >&2 echo "User overlays need to have extension .sh to be picked up!"
+        exit 1
+    fi
+done
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 9f24960ff..ecfdfab94 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -1,50 +1,159 @@
 #!/usr/bin/env bash
 
 set -e
+set -o pipefail
+
+API=https://api.github.com/repos/coq/coq
+OFFICIAL_REMOTE_URL="git@github.com:coq/coq"
 
 # This script depends (at least) on git and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
 
-#TODO: check arguments and show usage if relevant
+RED="\033[31m"
+RESET="\033[0m"
+GREEN="\033[32m"
+BLUE="\033[34m"
+YELLOW="\033[33m"
+info() {
+  echo -e "${GREEN}info:${RESET} $1 ${RESET}"
+}
+error() {
+  echo -e "${RED}error:${RESET} $1 ${RESET}"
+}
+warning() {
+  echo -e "${YELLOW}warning:${RESET} $1 ${RESET}"
+}
 
-PR=$1
+check_util() {
+if ! command -v "$1" > /dev/null 2>&1; then
+  error "this script requires the $1 command line utility"
+  exit 1
+fi
+}
 
-CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
-REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
-git fetch "$REMOTE" "refs/pull/$PR/head"
+ask_confirmation() {
+  read -p "Continue anyway? [y/N] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+}
 
-API=https://api.github.com/repos/coq/coq
+check_util jq
+check_util curl
+check_util git
+check_util gpg
+
+# command line parsing
 
-BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+if [ $# != 1 ]; then
+  error "usage: $0 PR-number"
+  exit 1
+fi
+
+if [[ "$1" =~ ^[1-9][0-9]*$ ]]; then
+  PR=$1
+else
+  error "$1 is not a number"
+  exit 1
+fi
+
+# Fetching PR metadata
+
+PRDATA=$(curl -s "$API/pulls/$PR")
+
+TITLE=$(echo "$PRDATA" | jq -r '.title')
+info "title for PR $PR is ${BLUE}$TITLE"
+
+BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label')
+info "PR $PR targets branch ${BLUE}$BASE_BRANCH"
+
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
+
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+if [ -z "$REMOTE" ]; then
+  error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote"
+  error "don't know where to fetch the PR from"
+  error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
+  exit 1
+fi
+REMOTE_URL=$(git remote get-url "$REMOTE" --push)
+if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \
+     "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+  error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
+  error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
+  error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
+  ask_confirmation
+fi
+info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE"
 
+info "fetching from $REMOTE the PR"
+git remote update "$REMOTE"
+if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then
+  error "remote $REMOTE is not configured to fetch pull requests"
+  error "run: git config remote.$REMOTE.fetch +refs/pull/*/head:refs/remotes/$REMOTE/pr/*"
+  exit 1
+fi
+git fetch "$REMOTE" "refs/pull/$PR/head"
 COMMIT=$(git rev-parse FETCH_HEAD)
-STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+info "commit for PR $PR is ${BLUE}$COMMIT"
+
+# Sanity check: merge to a different branch
 
 if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
-  echo "Wrong base branch"
-  read -p "Bypass? [y/N] " -n 1 -r
-  echo
-  if [[ ! $REPLY =~ ^[Yy]$ ]]
-  then
-    exit 1
-  fi
+  error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
+  ask_confirmation
 fi;
 
-if [ "$STATUS" != "success" ]; then
-  echo "CI status is \"$STATUS\""
-  read -p "Bypass? [y/N] " -n 1 -r
-  echo
-  if [[ ! $REPLY =~ ^[Yy]$ ]]
-  then
-    exit 1
-  fi
+# Sanity check: CI failed
+
+STATUS=$(curl -s "$API/commits/$COMMIT/status")
+
+if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then
+  error "CI unsuccessful on ${BLUE}$(echo "$STATUS" |
+    jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
+  ask_confirmation
 fi;
 
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
+# Sanity check: has labels named "needs:"
+
+NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
+if [ "$NEEDS_LABELS" != "[]" ]; then
+  error "needs:something labels still present: ${BLUE}$NEEDS_LABELS"
+  ask_confirmation
+fi
+
+# Sanity check: has milestone
+
+MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title')
+if [ "$MILESTONE" = "null" ]; then
+  error "no milestone set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: has kind
+
+KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
+if [ "$KIND" = "[]" ]; then
+  error "no kind:something label set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: user.signingkey
+if [ -z "$(git config user.signingkey)" ]; then
+  warning "git config user.signingkey is empty"
+  warning "gpg will guess a key out of your git config user.* data"
+fi
+
+info "merging"
+git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e
 
 # TODO: improve this check
-if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
-  echo "******************************************"
-  echo "** WARNING: does this PR have overlays? **"
-  echo "******************************************"
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then
+  warning "this PR may have overlays (sorry the check is not perfect)"
+  warning "if it has overlays please check the following:"
+  warning "- each overlay has a corresponding open PR on the upstream repo"
+  warning "- after merging please notify the upstream they can merge the PR"
 fi
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index c9cdee84a..a514b8866 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -5,6 +5,8 @@
 
 set -e
 
+dev/tools/check-overlays.sh
+
 if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
         ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
 then