aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dune
diff options
context:
space:
mode:
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)