diff options
| author | Emilio Jesus Gallego Arias | 2019-03-12 12:07:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-12 12:17:22 +0100 |
| commit | 430851db6db8ba30280f024ccbca5f6124287ab7 (patch) | |
| tree | 0ec5fe772209c4cd30ed1ce55c5cf2e500b5bc34 | |
| parent | 591af507e606aef4bd97dc226567289b1a959cc1 (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.
| -rw-r--r-- | dev/doc/build-system.dune.md | 4 | ||||
| -rw-r--r-- | dev/shim/dune | 13 | ||||
| -rw-r--r-- | dune | 2 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 7 |
4 files changed, 23 insertions, 3 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/shim/dune b/dev/shim/dune index 85a0d205da..39b4ef492c 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -11,6 +11,19 @@ (run chmod +x %{targets}))))) (rule + (targets coqbyte-prelude) + (deps + %{bin:coqtop.byte} + %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to %{targets} + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule (targets coqide-prelude) (deps %{bin:coqqueryworker.opt} @@ -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) diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 62a871aa0e..98368d76ca 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -235,6 +235,12 @@ let scan_plugins m = let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in List.fold_left scan_mlg m dirs +(* This will be removed when we drop support for Make *) +let fix_cmo_cma file = + if String.equal Filename.(extension file) ".cmo" + then replace_ext ~file ~newext:".cma" + else file + (* Process .vfiles.d and generate a skeleton for the dune file *) let parse_coqdep_line l = match Str.(split (regexp ":") l) with @@ -249,6 +255,7 @@ let parse_coqdep_line l = the platform. Anyways, I hope we can link to coqdep instead of having to parse its output soon, that should solve this kind of issues *) + let deps = List.map fix_cmo_cma deps in Some (String.split_on_char '/' dir, VO { target; deps; }) (* Otherwise a vio file, we ignore *) | _ -> None |