5 files changed, 51 insertions, 32 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 63d5541f48..8620b01b26 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -226,3 +226,10 @@
 : "${quickchick_CI_REF:=master}"
 : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
+: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin-tutorial.sh
new file mode 100755
index 0000000000..6c26a71a21
--- /dev/null
+++ b/dev/ci/ci-plugin-tutorial.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download plugin_tutorial
+
+( cd "${CI_BUILD_DIR}/plugin_tutorial" && \
+  pushd tuto0 && make && popd          && \
+  pushd tuto1 && make && popd          && \
+  pushd tuto2 && make && popd          && \
+  pushd tuto3 && make && popd          )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8d0f69626e..fcfa591ce1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-24-V01"
+# CACHEKEY: "bionic_coq-V2018-09-25-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -32,33 +32,31 @@ ENV NJOBS="2" \
     OPAMYES="true"
 
 # Base opam is the set of base packages required by Coq
-ENV COMPILER="4.02.3"
+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.0 dune.1.2.1 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="6.14" \
+ENV CAMLP5_VER="7.01" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
-# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3
+# base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install ocamlfind.1.8.0 && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install ocamlfind.1.8.0 && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
-    BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0"
+    BASE_OPAM_EDGE="dune-release.0.3.0"
 
 RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 36d5e5841b..7349360be8 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -3,11 +3,15 @@ Dune-based build system. If you want to enhance the build system
 itself (or are curious about its implementation details), see
 build-system.dev.txt, and in particular its initial HISTORY section.
 
-Quick Start
-===========
+About Dune
+==========
+
+Coq can now be built using [Dune](https://github.com/ocaml/dune).
+
+## Quick Start
 
 You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq
-libraries. No `./configure` step is needed.
+libraries. No call to `./configure` is needed.
 
 Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
@@ -18,31 +22,26 @@ call `make -f Makefile.dune voboot`. It is usually enough to do that
 once per-session.
 
 More helper targets are availabe in `Makefile.dune`, `make -f
-Makefile.dune` will display help.
+Makefile.dune` will display some help.
 
-Dune
-====
+Dune places build artifacts in a separate directory `_build`; it will
+also generate an `.install` file so files can be properly installed by
+package managers.
 
-Coq can now be built using
-[Dune](https://github.com/ocaml/dune). Contrary to other systems,
-Dune, doesn't use a global`makefile` but local build files named
-`dune` that are later composed to form a global build.
+Contrary to other systems, Dune doesn't use a global `Makefile` but
+local build files named `dune` that are later composed to form a
+global build.
 
 As a developer, Dune should take care of all OCaml-related build tasks
-including library management, merlin files, and link order. You are
+including library management, merlin files, and linking order. You are
 are not supposed to modify the `dune` files unless you are adding a
 new binary, library, or plugin.
 
-The current Dune setup also doesn't require a call to `configure`. The
-auto-generated configuration files are properly included in the
-dependency graph so it will be automatically generated by Dune with
-reasonable developer defaults. You can still override the defaults by
-manually calling `./configure`, but note that some configure options
-such as install paths are not used by Dune.
+## Per-User Custom Settings
 
-Dune uses a separate directory `_build` to store build artifacts; it
-will generate an `.install` file so artifacts in the build can be
-properly installed by package managers.
+Dune will read the file `~/.config/dune/config`; see `man
+dune-config`. Among others, you can set in this file the custom number
+of build threads `(jobs N)` and display options `(display _mode_)`.
 
 ## Targets
 
@@ -53,8 +52,10 @@ project, creating an "install" overlay in `_build/install/default`.
 You can build some other target by doing `dune build $TARGET`.
 
 In order to build a single package, you can do `dune build
-$PACKAGE.install`. Dune also provides targets for documentation and
-testing, see below.
+$PACKAGE.install`.
+
+Dune also provides targets for documentation, testing, and release
+builds, please see below.
 
 ## Developer shell
 
@@ -83,7 +84,8 @@ current Coq source tree contains two packages [Coq and CoqIDE], and in
 the OPAM CoqIDE package we don't want to build CoqIDE against the
 local copy of Coq. For this purpose, Dune supports the `-p` option, so
 `dune build -p coqide` will build CoqIDE against the system-installed
-version of Coq libs.
+version of Coq libs, and use a "release" profile that for example
+enables stronger compiler optimizations.
 
 ## Stanzas
 
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 45766293c7..29e87df6b8 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.3+fp
+opam switch 4.05.0+trunk+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v