From 33cc626936d2c05a98ebf6d2e31bda7217c030b1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Nov 2018 04:03:40 +0100
Subject: [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.
---
 tools/coq_dune.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tools')

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 =
-- 
cgit v1.2.3