From 9870e1f8662923d0de1b9c2014d3b4f647a893da Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 21 Nov 2018 20:16:49 +0100
Subject: [dune] Shim for starting `coqtop/coqide` with minimal config.

As requested by Gaëtan Gilbert, we add shims

- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`

that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.

`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states && bin/coqtop` under the old model.

This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.

In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]

We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.

The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.

This will work for `dir=stdlib/Init/` for example, or for any other
combination.
---
 Makefile.dune                |  8 ++++----
 dev/doc/build-system.dune.md | 18 ++++++++++++++++++
 dev/shim/dune                | 27 +++++++++++++++++++++++++++
 3 files changed, 49 insertions(+), 4 deletions(-)
 create mode 100644 dev/shim/dune

diff --git a/Makefile.dune b/Makefile.dune
index 7dd9914c6e..4609c563d9 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -41,12 +41,14 @@ help:
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
 
+# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work.
 voboot:
+	@echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune
 	dune build $(DUNEOPT) @vodeps
 	dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d
 
 states: voboot
-	dune build $(DUNEOPT) theories/Init/Prelude.vo
+	dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude
 
 world: voboot
 	dune build $(DUNEOPT) @install
@@ -79,9 +81,7 @@ quickopt: voboot
 	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
 
 quickide: states
-	dune build $(DUNEOPT) @topworkers
-	dune build $(DUNEOPT) coqide-server.install
-	dune build $(DUNEOPT) coqide.install
+	dune build $(DUNEOPT) dev/shim/coqide-prelude
 
 test-suite: voboot
 	dune runtest --no-buffer $(DUNEOPT)
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})))))
-- 
cgit v1.2.3