aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-12 12:07:56 +0100
committerEmilio Jesus Gallego Arias2019-03-12 12:17:22 +0100
commit430851db6db8ba30280f024ccbca5f6124287ab7 (patch)
tree0ec5fe772209c4cd30ed1ce55c5cf2e500b5bc34 /dune
parent591af507e606aef4bd97dc226567289b1a959cc1 (diff)
[dune] Add shim for coqtop.byte
We add a shim for running the byte version of coqtop. This fixes the Coq part of #9727 , the Dune part is still open at https://github.com/ocaml/dune/issues/108 but this PR includes a workaround. Unfortunately we have to introduce a small inefficiency in the build process as we build both byte and native versions of plugins for this work reliable. As this is a choice done during bootstrap it won't be easy to fix until we have our own `dune coqtop` command and we can control the rules depending on the final target. This should affect the `check` target so still fast builds should be possible, but if this is a problem we could add a `byteboot` target to help.
Diffstat (limited to 'dune')
-rw-r--r--dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/dune b/dune
index 32dbc736f3..f1f966b7fd 100644
--- a/dune
+++ b/dune
@@ -19,7 +19,7 @@
(deps
(source_tree theories)
(source_tree plugins))
- (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`"))))
+ (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins -type f -name *.v`"))))
(alias
(name vodeps)