[coqtop] fix directory for subdirectory targets.

This was reported in ocaml#5552.

Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Signed-off-by: Rodolphe Lepigre <lepigre@mpi-sws.org>

CHANGES.md

@@ -13,6 +13,10 @@
 3.3.0 (17-06-2022)
 ------------------
 
+- Fix ``dune coq top`` when it is invoked on files from a subdirectory of the
+  directory containing the associated stanza (#5784, fixes #5552, @ejgallego,
+  @rlepigre)
+
 - Sandbox preprocessing, lint, and dialect rules by default. All these rules
   now require precise dependency specifications (#5807, @rgrinberg)
 

bin/coqtop.ml

@@ -39,18 +39,20 @@ let term =
         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 =
-          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
+          if Filename.is_relative coq_file_arg then coq_file_arg
+          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 = Common.prefix_target common coq_file_arg in
@@ -64,6 +66,14 @@ let term =
         let* coqtop, args =
           let open Memo.O in
           Build_system.run_exn (fun () ->
+              let* (tr : Dune_rules.Dir_contents.triage) =
+                Dune_rules.Dir_contents.triage sctx ~dir
+              in
+              let dir =
+                match tr with
+                | Group_part dir -> dir
+                | Standalone_or_root _ -> dir
+              in
               let* dc = Dune_rules.Dir_contents.get sctx ~dir in
               let* coq_src = Dune_rules.Dir_contents.coq dc in
               let coq_module =

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

@@ -0,0 +1,3 @@
+(lang dune 3.0)
+
+(using coq 0.3)

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

@@ -0,0 +1,16 @@
+Checking that we compute the directory and file for dune coq top correctly
+
+  $ dune build --display=short theories/c.vo
+        coqdep theories/c.v.d
+        coqdep theories/d.v.d
+          coqc theories/.d.aux,theories/d.{glob,vo}
+          coqc theories/.c.aux,theories/c.{glob,vo}
+  $ dune build --display=short theories/b/b.vo
+        coqdep theories/b/b.v.d
+        coqdep theories/a/a.v.d
+          coqc theories/a/.a.aux,theories/a/a.{glob,vo}
+          coqc theories/b/.b.aux,theories/b/b.{glob,vo}
+  $ dune coq top --toplevel=echo theories/c.v
+  -topfile $TESTCASE_ROOT/_build/default/theories/c.v -R $TESTCASE_ROOT/_build/default/theories foo
+  $ dune coq top --toplevel=echo theories/b/b.v
+  -topfile $TESTCASE_ROOT/_build/default/theories/b/b.v -R $TESTCASE_ROOT/_build/default/theories foo

test/blackbox-tests/test-cases/coq/coqtop-nested.t/theories/a/a.v

@@ -0,0 +1 @@
+Definition bar := 3.

test/blackbox-tests/test-cases/coq/coqtop-nested.t/theories/b/b.v

@@ -0,0 +1,3 @@
+Require a.
+
+Definition moo := a.bar.

test/blackbox-tests/test-cases/coq/coqtop-nested.t/theories/c.v

@@ -0,0 +1,3 @@
+Require d.
+
+Definition uuhh := d.aike.

test/blackbox-tests/test-cases/coq/coqtop-nested.t/theories/d.v

@@ -0,0 +1 @@
+Definition aike := 3.

test/blackbox-tests/test-cases/coq/coqtop-nested.t/theories/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name foo))
+
+(include_subdirs qualified)