fixup install locations in Path.make (not sure if this is the right p…

…lace)

tools/dune_rule_gen/coq_rules.ml

@@ -70,7 +70,7 @@ let cmi_of_dep ~tname dep =
   let open Coqdeplib.Dep_info in
   let file = match dep with
     | Dep.Require dep ->
-      Some (translate_to_native ~tname dep)
+      Some (translate_to_native ~tname  dep)
     | Dep.Ml _dep-> None
     | Dep.Other _ -> None
   in
@@ -171,11 +171,6 @@ module Context = struct
 
 end
 
-(* Super hack, to be removed *)
-let fixup_install_locations file =
-  Str.replace_first (Str.regexp {|\(\.\./\)*../install|})
-    "%{project_root}/_build/install" file
-
 (* Return flags and deps to inject *)
 let prelude_path = "Init/Prelude.vo"
 
@@ -214,7 +209,6 @@ let module_rule ~(cctx : Context.t) coq_module =
   let lvl = cctx.root_lvl + (Coq_module.prefix coq_module |> List.length) in
   let flags = (* flags are relative to the root path *) Arg.List.to_string (flags @ timeflags) in
   let deps = List.map (Path.adjust ~lvl) vfile_deps |> List.map Path.to_string in
-  let deps = List.map fixup_install_locations deps in
   (* Depend on the workers if async *)
   let deps = cctx.async_deps @ deps in
   (* Build rule *)

tools/dune_rule_gen/path.ml

@@ -10,7 +10,25 @@ type t = Rel of string | Abs of string
 
 let to_string = function Rel p -> p | Abs p -> p
 
-let make path = if Filename.is_relative path then Rel path else Abs path
+let make path =
+  if Filename.is_relative path then
+    (* when called by dune, the cmxs and META files are in
+       ../install/... relative to cwd (= _build/default)
+       but the generated dune file will be moved to ../theories
+       so adjusting the path to be relative to the .v won't work
+
+       (it would be relative to the .v in
+       project_root/_build/default/theories but dune would read it as
+       relative to the .v in project_root/theories, the number of ..
+       to insert to get to project_root doesn't match) *)
+    if CString.is_prefix ".." path then
+      Abs (Filename.concat "%{project_root}" @@
+           Filename.concat "_build" @@
+           String.sub path 3 (String.length path - 3))
+    else
+      Rel path
+  else
+    Abs path
 
 let map ~f = function Rel p -> Rel (f p) | Abs p -> Abs (f p)