7 files changed, 74 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 74e8d3bbaa..deeec3942d 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -289,3 +289,10 @@
 : "${verdi_raft_CI_REF:=master}"
 : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
 : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
+
+########################################################################
+# stdlib2
+########################################################################
+: "${stdlib2_CI_REF:=master}"
+: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
+: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh
new file mode 100755
index 0000000000..ec1c180d7d
--- /dev/null
+++ b/dev/ci/ci-stdlib2.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download stdlib2
+
+( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install)
diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
new file mode 100644
index 0000000000..1af8b5430d
--- /dev/null
+++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then
+
+    quickchick_CI_REF=context-constructor
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    equations_CI_REF=context-constructor
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 5705857d76..3f1b470878 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -37,6 +37,9 @@ When maintainers receive a review request, they are expected to:
   REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
   process described below.
 
+To know what files you are a code owner of in a large PR, you can run
+`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect.
+
 When a PR received lots of comments or if the PR has not been opened for long
 and the assignee thinks that some other developers might want to comment,
 it is recommended that they announce their intention to merge and wait a full
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index da91c85856..a31ab1c511 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -44,6 +44,24 @@ 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_)`.
 
+## 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:
+
+```
+$ 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.
+
+Note that for a fast developer build of ML files, the `check` target
+will be faster.
+
 ## Targets
 
 The default dune target is `dune build` (or `dune build @install`),
diff --git a/dev/shim/dune b/dev/shim/dune
new file mode 100644
index 0000000000..85a0d205da
--- /dev/null
+++ b/dev/shim/dune
@@ -0,0 +1,27 @@
+(rule
+ (targets coqtop-prelude)
+ (deps
+  %{bin:coqtop}
+  %{project_root}/theories/Init/Prelude.vo)
+ (action
+  (with-outputs-to coqtop-prelude
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
+
+(rule
+ (targets coqide-prelude)
+ (deps
+  %{bin:coqqueryworker.opt}
+  %{bin:coqtacticworker.opt}
+  %{bin:coqproofworker.opt}
+  %{project_root}/theories/Init/Prelude.vo
+  %{project_root}/coqide-server.install
+  %{project_root}/coqide.install)
+ (action
+  (with-outputs-to coqide-prelude
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index ec72f96509..c6687b9731 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -80,9 +80,8 @@ Note that this function is executed before _Coqproject is read if it exists."
     (when dir
       (unless coq-prog-args
         (setq coq-prog-args
-              `("-coqlib" ,dir "-R" ,(concat dir "plugins")
-                "Coq" "-R" ,(concat dir "theories")
-                "Coq")))
+              `("-coqlib" ,dir
+                "-topfile" ,buffer-file-name)))
       (setq-local coq-prog-name (concat dir "bin/coqtop")))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)