aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dune
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-04 09:46:41 +0100
committerThéo Zimmermann2019-03-04 09:46:41 +0100
commit913e377f3d24274215bd7d9d37c0189b8b5eb4a6 (patch)
tree01b7902da80ed35e0b58b54e283996ac8b0054ca /Makefile.dune
parent53240d3248ce1fb36ab99036186eda9051fbb068 (diff)
parent9870e1f8662923d0de1b9c2014d3b4f647a893da (diff)
Merge PR #9047: [dune] Shim for starting `coqtop/coqide` with minimal config.
Reviewed-by: Zimmi48 Ack-by: rgrinberg
Diffstat (limited to 'Makefile.dune')
-rw-r--r--Makefile.dune8
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)