9 files changed, 93 insertions, 24 deletions
diff --git a/dev/Bugzilla_Coq_autolink.user.js b/dev/Bugzilla_Coq_autolink.user.js
new file mode 100644
index 0000000000..ed056021b3
--- /dev/null
+++ b/dev/Bugzilla_Coq_autolink.user.js
@@ -0,0 +1,25 @@
+// ==UserScript==
+// @name        Bugzilla Coq autolink
+// @namespace   CoqScript
+// @include     https://coq.inria.fr/bugs/*
+// @description Makes #XXXX into links to Github Coq PRs
+// @version     1
+// @grant       none
+// ==/UserScript==
+
+var regex = /#(\d+)/g;
+var substr = '<a href="https://github.com/coq/coq/pull/$1">$&</a>';
+
+function doNode(node)
+{
+    node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("bz_comment_table")[0];
+var pars = comments.getElementsByClassName("bz_comment_text");
+
+for(var j=0; j<pars.length; j++)
+{
+    doNode(pars[j]);
+}
+
diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js
new file mode 100644
index 0000000000..371c5adc00
--- /dev/null
+++ b/dev/Coq_Bugzilla_autolink.user.js
@@ -0,0 +1,34 @@
+// ==UserScript==
+// @name        Coq Bugzilla autolink
+// @namespace   SkySkimmer
+// @include     https://github.com/coq/coq/*
+// @description Makes BZ#XXXX into links to bugzilla for GitHub
+// @version     1
+// @grant       none
+// ==/UserScript==
+
+var regex = /BZ#(\d+)/g;
+var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>';
+
+function doNode(node)
+{
+    node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("comment-body");
+
+for(var i=0; i<comments.length; i++)
+{
+    var pars = comments[i].getElementsByTagName("p");
+    for(var j=0; j<pars.length; j++)
+    {
+        doNode(pars[j]);
+    }
+}
+
+// usually 1 or 0 titles...
+var titles = document.getElementsByClassName("js-issue-title");
+for(var i=0; i<titles.length; i++)
+{
+    doNode(titles[i]);
+}
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f3e4cec0b9..f12cbe0a78 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -910,6 +910,10 @@ function make_camlp5 {
     log2 make install
     # For some reason gramlib.a is not copied, but it is required by Coq
     cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
+    # For some reason META is not copied, but it is required by coq_makefile
+    log2 make -C etc META
+    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
     log2 make clean
     build_post
   fi
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index ca6a5643c1..e2fbf1f6d1 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -23,13 +23,19 @@ if %USEOPAM% == false (
   call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
     -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
     -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-    -setup %CYGROOT%\%SETUP%
-  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis
-  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\*
+    -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
+  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
 )
 
 if %USEOPAM% == true (
   %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
     -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
-  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh
+  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
 )
+
+GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR MakeCoq_MinGW.bat failed
+  EXIT /b 1
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8e7265969b..43525dcd40 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -127,5 +127,5 @@
 ########################################################################
 # Bignums
 ########################################################################
-: ${bignums_CI_BRANCH:=fix-thunk-printer}
-: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git}
+: ${bignums_CI_BRANCH:=master}
+: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index eadeb7c38c..8e6448e764 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -8,9 +8,5 @@ GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
 git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
 
 ( cd ${GeoCoq_CI_DIR}                                     && \
-  ./configure.sh                                          && \
-  sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
-  sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
-  sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
-  coq_makefile -f Make -o Makefile                        && \
+  ./configure-ci.sh                                       && \
   make )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 2d127ddc1b..c49b6ed9c9 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -9,17 +9,19 @@ Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
 
 install_ssreflect
 
-# Setup Iris first, as it is needed to compute the dependencies
+# Add or update the opam repo we need for dependency resolution
+opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
 
+# Setup Iris first, extract required version of std++
 git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
-read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins
+stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o)
 
-# Setup stdpp
-stdpp_CI_GITURL=${IRIS_DEP[1]}.git
-stdpp_CI_COMMIT=${IRIS_DEP[2]}
-
-git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
+# Ask opam where to get this std++, separating at the #
+stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url)
+read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ')
 
+# Setup std++
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]}
 ( cd ${stdpp_CI_DIR} && make && make install )
 
 # Build iris now
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 5ed74917aa..b5e19f33c3 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -641,6 +641,12 @@ The main search functions now take a function iterating over the
 results. This allows for clients to use streaming or more economic
 printing.
 
+### XML Protocol
+
+- In several places, flat text wrapped in `<string>` tags now appears as structured text inside `<richpp>` tags.
+
+- The "errormsg" feedback has been replaced by a "message" feedback which contains `<feedback\_content>` tag, with a message_level attribute of "error".
+
 ## Changes between Coq 8.4 and Coq 8.5
 
 ### Refactoring : more mli interfaces and simpler grammar.cma
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index cf7d205d8b..18f6288f6f 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -1,4 +1,4 @@
-#Coq XML Protocol for Coq 8.6#
+# Coq XML Protocol
 
 This document is based on documentation originally written by CJ Bell
 for his [vscoq](https://github.com/siegebell/vscoq/) project.
@@ -12,11 +12,7 @@ A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md).
 OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli).
 
-# CHANGES
-## Changes from 8.5:
- * In several places, flat text wrapped in <string> tags now appears as structured text inside <richpp> tags 
- * The "errormsg" feedback has been replaced by a "message" feedback which contains
-    <feedback\_content> tag, with a message_level attribute of "error"
+Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
 
 * [Commands](#commands)
   - [About](#command-about)