diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 04:03:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-05 18:52:14 +0100 |
| commit | 33cc626936d2c05a98ebf6d2e31bda7217c030b1 (patch) | |
| tree | 9bcd5b1e388938d75f3cb42f8d147234982aa3b7 | |
| parent | efe60d3c1b09bc059053b7383e068ddc05248dac (diff) | |
[dune] Add to vo rules explicit location of coqlib in boot mode.
When `-coqlib $PATH` is absent, Coq will try to locate coqlib using a
heuristic based on the name of the executable.
The code in `envars.ml` basically does:
```ocaml
Filename.(dirname CUnix.(canonical_path_name (dirname Sys.executable_name)))
```
which doesn't seem to work very well on Windows and OSX when `coqtop`
is a symlink.
Instead, we now pass the right `-coqlib` to coqtop from `coq_dune`.
Maybe fixes #8862.
| -rw-r--r-- | tools/coq_dune.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index f94da14cd0..84850e7158 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -175,8 +175,10 @@ let pp_vo_dep dir fmt vo = let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in + (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) + let libflag = "-coqlib %{project_root}" in (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in + let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in pp_rule fmt [vo.target] deps action let pp_ml4_dep _dir fmt ml = |