4 files changed, 31 insertions, 16 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b8f9d99702..41392b4b8c 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-12-08-V82"
+# CACHEKEY: "bionic_coq-V2019-03-01-V43"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,9 +37,9 @@ 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 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.8.0"
+    BASE_ONLY_OPAM="elpi.1.10.2"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6"
diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
deleted file mode 100644
index 7845654375..0000000000
--- a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then
-
-    elpi_CI_REF="coq-master+v1.2"
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh
new file mode 100644
index 0000000000..121190e5f6
--- /dev/null
+++ b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11708" ] || [ "$CI_BRANCH" = " elpi-1.10+coq-elpi-1.3" ]; then
+
+    elpi_CI_REF="coq-master+coq-elpi-1.3"
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index cd35064b18..777eec97c6 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -46,21 +46,27 @@ of build threads `(jobs N)` and display options `(display _mode_)`.
 
 ## Running binaries [coqtop / coqide]
 
-There are two special targets `states` and `quickide` that will
-generate "shims" for running `coqtop` and `coqide` in a fast build. In
-order to use them, do:
+Running `coqtop` directly with `dune exec -- coqtop` won't in general
+work well unless you are using `dune exec -- coqtop -noinit`. The
+`coqtop` binary doesn't depend itself on Coq's prelude, so plugins /
+vo files may go stale if you rebuild only `coqtop`.
+
+Instead, you should use the provided "shims" for running `coqtop` and
+`coqide` in a fast build. In order to use them, do:
 
 ```
 $ make -f Makefile.dune voboot                # Only once per session
 $ dune exec -- dev/shim/coqtop-prelude
 ```
 
-or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
-enjoy quick incremental compilation thanks to `-opaque` so they tend
-to be very fast while developing.
+or `quickide` / `dev/shim/coqide-prelude` for CoqIDE, etc.... See
+`dev/shim/dune` for a complete list of targets. These targets enjoy
+quick incremental compilation thanks to `-opaque` so they tend to be
+very fast while developing.
 
 Note that for a fast developer build of ML files, the `check` target
-will be faster.
+is faster, as it doesn't link the binaries and uses the non-optimizing
+compiler.
 
 ## Targets
 
@@ -214,3 +220,12 @@ useful to Coq, some examples are:
 - Cross-compilation.
 - Automatic Generation of OPAM files.
 - Multi-directory libraries.
+
+## FAQ
+
+- I get "Error: Dynlink error: Interface mismatch":
+
+  You are likely running a partial build which doesn't include
+  implicitly loaded plugins / vo files. See the "Running binaries
+  [coqtop / coqide]" section above as to how to correctly call Coq's
+  binaries.