diff options
| -rw-r--r-- | Makefile.dune | 8 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 18 | ||||
| -rw-r--r-- | dev/shim/dune | 27 |
3 files changed, 49 insertions, 4 deletions
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}))))) |