Merge PR rocq-prover#19899: [build] Fix wrong use of %{project_root}/_build in config files

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

Author: coqbot-app[bot]

dev/shim/dune

@@ -18,7 +18,26 @@
   (with-stdout-to %{targets}
    (progn
     (echo "#!/usr/bin/env bash\n")
-    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{workspace_root}/_build/install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
+    (run chmod +x %{targets})))))
+
+; coqidetop
+
+(alias
+ (name coqidetop-prelude)
+ (deps
+  %{bin:coqidetop.opt}
+   ; XXX: bug, we are missing the dep on the _install meta file...
+  %{project_root}/theories/Init/Prelude.vo))
+
+(rule
+ (targets coqidetop.opt)
+ (deps (alias coqidetop-prelude))
+ (action
+  (with-stdout-to %{targets}
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqidetop.opt} -I \"$(dirname \"$0\")/%{workspace_root}/_build/install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
     (run chmod +x %{targets})))))
 
 ; coqc
@@ -37,7 +56,7 @@
   (with-stdout-to %{targets}
    (progn
     (echo "#!/usr/bin/env bash\n")
-    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} -nI \"$(dirname \"$0\")\"/%{project_root}/kernel/.kernel.objs/byte \"$@\"'")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{workspace_root}/_build/install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} -nI \"$(dirname \"$0\")\"/%{project_root}/kernel/.kernel.objs/byte \"$@\"'")
     (run chmod +x %{targets})))))
 
 ; coqtop.byte
@@ -80,7 +99,7 @@
   (with-stdout-to %{targets}
    (progn
     (echo "#!/usr/bin/env bash\n")
-    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{workspace_root}/_build/install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
     (run chmod +x %{targets})))))
 
 ; coqide
@@ -91,7 +110,7 @@
   ; without this if the gtk libs are not available dune can try to use
   ; coqide from PATH instead of giving a nice error
   ; there is no problem with the other shims since they don't depend on optional build products
-  %{project_root}/ide/coqide/coqide_main.exe
+  %{project_root}/ide/coqide/rocqide_main.exe
   %{bin:coqworker.opt}
   %{project_root}/theories/Init/Prelude.vo
   %{project_root}/coqide-server.install
@@ -104,5 +123,5 @@
   (with-stdout-to %{targets}
    (progn
     (echo "#!/usr/bin/env bash\n")
-    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqide} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
+    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqide} -I \"$(dirname \"$0\")/%{workspace_root}/_build/install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
     (run chmod +x %{targets})))))

dune

@@ -41,7 +41,7 @@
   (source_tree plugins)
   (source_tree theories)
   (source_tree user-contrib)
-  %{project_root}/_build/install/%{context_name}/lib/coq-core/META)
+  %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META)
  (action
   (with-stdout-to %{targets}
    (run tools/dune_rule_gen/gen_rules.exe Corelib theories %{env:COQ_DUNE_EXTRA_OPT=}))))
@@ -52,7 +52,7 @@
   (source_tree plugins)
   (source_tree theories)
   (source_tree user-contrib)
-  %{project_root}/_build/install/%{context_name}/lib/coq-core/META)
+  %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META)
  (action
   (with-stdout-to %{targets}
    (run tools/dune_rule_gen/gen_rules.exe Ltac2 user-contrib/Ltac2 %{env:COQ_DUNE_EXTRA_OPT=}))))

tools/coqdep/lib/dune

@@ -7,7 +7,7 @@
 
 (rule
  (targets static_toplevel_libs.ml)
- (deps %{project_root}/_build/install/%{context_name}/lib/coq-core/META)
+ (deps %{workspace_root}/_build/install/%{context_name}/lib/coq-core/META)
  (action
   (with-stdout-to %{targets}
    (run ocamlfind query -recursive -predicates native coq-core.toplevel

tools/dune_rule_gen/coq_rules.ml

@@ -51,11 +51,11 @@ let path_of_dep ~vo_ext dep =
      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
+     workspace_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) *)
   let file = if CString.is_prefix ".." file then
-      (Filename.concat "%{project_root}" "_build")
+      (Filename.concat "%{workspace_root}" "_build")
       ^ String.sub file 2 (String.length file - 2)
     else file
   in