diff options
| author | Emilio Jesus Gallego Arias | 2018-11-21 20:16:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-03 17:21:13 +0100 |
| commit | 9870e1f8662923d0de1b9c2014d3b4f647a893da (patch) | |
| tree | 01b7902da80ed35e0b58b54e283996ac8b0054ca /Makefile.dune | |
| parent | 53240d3248ce1fb36ab99036186eda9051fbb068 (diff) | |
[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.
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 8 |
1 files changed, 4 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) |