Fix for 7344.

bin/coq/coqtop.ml

@@ -31,42 +31,24 @@ let term =
     Arg.(value & pos_right 0 string [] (Arg.info [] ~docv:"ARGS"))
   in
   let config = Common.init common in
-  let root = Common.root common in
-  let prefix_target = Common.prefix_target common in
+  let coq_file_arg =
+    Common.prefix_target common coq_file_arg |> Path.Local.of_string
+  in
   let coqtop, argv, env =
     Scheduler.go ~common ~config (fun () ->
         let open Fiber.O in
         let* setup = Import.Main.setup () in
         let* setup = Memo.run setup in
         let sctx = Import.Main.find_scontext_exn setup ~name:context in
         let context = Dune_rules.Super_context.context sctx in
-        (* Try to compute a relative path if we got an absolute path. *)
-        let coq_file_arg =
-          if Filename.is_relative coq_file_arg then
-            Path.relative Path.root (root.reach_from_root_prefix ^ coq_file_arg)
-            |> Path.to_string
-          else
-            let cwd = Path.external_ Path.External.initial_cwd in
-            let file =
-              (* Best-effort symbolic link unfolding. *)
-              let file = Fpath.follow_symlinks coq_file_arg in
-              Option.value file ~default:coq_file_arg
-            in
-            let file = Path.of_filename_relative_to_initial_cwd file in
-            let cwd = Path.to_string cwd in
-            let file = Path.to_string file in
-            match String.drop_prefix ~prefix:(cwd ^ "/") file with
-            | None -> coq_file_arg
-            | Some s -> s
-        in
         let coq_file_build =
-          let p = prefix_target coq_file_arg in
-          Path.Build.relative context.build_dir p
+          Path.Build.append_local context.build_dir coq_file_arg
         in
         let dir =
-          let dir = Filename.dirname coq_file_arg in
-          let p = prefix_target dir in
-          Path.Build.relative context.build_dir p
+          (match Path.Local.parent coq_file_arg with
+          | None -> Path.Local.root
+          | Some dir -> dir)
+          |> Path.Build.append_local context.build_dir
         in
         let* coqtop, args =
           Build_system.run_exn @@ fun () ->
@@ -87,12 +69,14 @@ let term =
             | Some m -> snd m
             | None ->
               let hints =
-                [ Pp.textf "is the file part of a stanza?"
-                ; Pp.textf "has the file been written to disk?"
+                [ Pp.textf "Is the file part of a stanza?"
+                ; Pp.textf "Has the file been written to disk?"
                 ]
               in
               User_error.raise ~hints
-                [ Pp.textf "cannot find file: %s" coq_file_arg ]
+                [ Pp.textf "Cannot find file: %s"
+                    (coq_file_arg |> Path.Local.to_string)
+                ]
           in
           let stanza =
             Dune_rules.Coq_sources.lookup_module coq_src coq_module
@@ -101,7 +85,9 @@ let term =
             match stanza with
             | None ->
               User_error.raise
-                [ Pp.textf "file not part of any stanza: %s" coq_file_arg ]
+                [ Pp.textf "File not part of any stanza: %s"
+                    (coq_file_arg |> Path.Local.to_string)
+                ]
             | Some (`Theory theory) ->
               ( Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir
                   ~dir_contents:dc theory coq_module

test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-stanza.t

@@ -8,7 +8,7 @@ Running the Coq Toplevel on a file that is not part of a stanza.
   > (using coq 0.3)
   > EOF
   $ dune coq top foo.v || echo failed
-  Error: cannot find file: foo.v
-  Hint: is the file part of a stanza?
-  Hint: has the file been written to disk?
+  Error: Cannot find file: foo.v
+  Hint: Is the file part of a stanza?
+  Hint: Has the file been written to disk?
   failed

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dune

@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory2))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory1))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dune

@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory4))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory3))

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/run.t

@@ -0,0 +1,108 @@
+Running "dune coq top" from different directories in a workspace. The setup is
+a workspace whose root is the root of a first project, and a second project is
+contained under directory "project".
+
+  $ unset INSIDE_DUNE
+  $ . ./util.sh
+
+Calling "dune coq top" from the workspace root.
+
+  $ coqtop_test file1.v
+  $ coqtop_test coq_dir1/file2.v
+  $ coqtop_test coq_dir1/dir1/file3.v
+  $ coqtop_test project/file4.v
+  $ coqtop_test project/coq_dir2/file5.v
+  $ coqtop_test project/coq_dir2/dir2/file6.v
+
+Calling "dune coq top" from the "coq_dir1" directory.
+
+  $ cd coq_dir1
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file2.v
+  $ coqtop_test dir1/file3.v
+
+  $ cd ..
+
+Calling "dune coq top" from the "coq_dir1/dir1" directory.
+
+  $ cd coq_dir1/dir1
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file2.v
+  $ coqtop_test ../dir1/file3.v
+  $ coqtop_test file3.v
+
+  $ cd ../..
+
+Calling "dune coq top" from the "project" directory.
+
+  $ cd project
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file4.v
+  $ coqtop_test coq_dir2/file5.v
+  $ coqtop_test coq_dir2/dir2/file6.v
+
+  $ cd ..
+
+Calling "dune coq top" from the "project/coq_dir2" directory.
+
+  $ cd project/coq_dir2
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file4.v
+  $ coqtop_test ../coq_dir2/file5.v
+  $ coqtop_test ../coq_dir2/dir2/file6.v
+  $ coqtop_test file5.v
+  $ coqtop_test dir2/file6.v
+
+  $ cd ../..
+
+Calling "dune coq top" from the "project/coq_dir2/dir2" directory.
+
+  $ cd project/coq_dir2/dir2
+
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../coq_dir1/file2.v
+  $ coqtop_test ../../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../../project/file4.v
+  $ coqtop_test ../../../project/coq_dir2/file5.v
+  $ coqtop_test ../../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../../file4.v
+  $ coqtop_test ../../coq_dir2/file5.v
+  $ coqtop_test ../../coq_dir2/dir2/file6.v
+  $ coqtop_test ../file5.v
+  $ coqtop_test ../dir2/file6.v
+  $ coqtop_test file6.v
+
+  $ cd ../../..

test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/util.sh

@@ -0,0 +1,5 @@
+OUTPUT="$PWD/coqtop_test.tmp"
+
+coqtop_test() {
+  (true | (dune coq top "$1" 1>$OUTPUT 2>&1)) || cat $OUTPUT
+}