Rocq output test name alias

src/dune_rules/rocq/rocq_rules.ml

@@ -820,14 +820,26 @@ let setup_output_diff_rule ~loc ~dir ~sctx ~rocq_lang_version ~rocq_sources rocq
       ; directory_diffs = true
       }
     in
-    let alias = Alias.make ~dir Alias0.runtest in
+    let alias_dir = Path.Build.parent_exn expected in
+    let name = Path.Build.basename expected |> Filename.remove_extension in
+    let alias_name = Alias.Name.of_string (Filename.to_string name) in
+    let alias = Alias.make ~dir:alias_dir alias_name in
+    let runtest_alias = Alias.make ~dir:alias_dir Alias0.runtest in
     Simple_rules.Alias_rules.add
       sctx
       ~loc
       ~alias
       (let open Action_builder.O in
        let+ () = Action_builder.paths [ diff.file1; Path.build diff.file2 ] in
        Action.Full.make (Action.Diff diff))
+    >>>
+    if Alias.Name.equal alias_name Alias0.runtest
+    then Memo.return ()
+    else
+      Rules.Produce.Alias.add_deps
+        runtest_alias
+        ~loc
+        (Action_builder.dep (Dep.alias alias))
 ;;
 
 let setup_rocqc_rule

test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t

@@ -0,0 +1,58 @@
+Testing that the diff rules are attached to the @runtest alias of the right
+directory. This used to not be the case, and these rules would be attached
+to the @runtest alias of the directory defining the rocq.theory stanza, even
+for files living in its sub-directories.
+
+  $ make_rocq_project 3.22 0.12
+
+  $ cat > dune <<EOF
+  > (include_subdirs qualified)
+  > (rocq.theory
+  >  (name a))
+  > EOF
+
+  $ mkdir sub
+  $ cat > sub/foo.v <<EOF
+  > Locate bool.
+  > EOF
+  $ touch sub/foo.expected
+
+This has always worked:
+
+  $ dune runtest
+  File "sub/foo.expected", line 1, characters 0-0:
+  --- sub/foo.expected
+  +++ sub/foo.output
+  @@ -0,0 +1 @@
+  +Inductive Corelib.Init.Datatypes.bool
+  [1]
+
+And this used to fail:
+
+  $ dune runtest sub
+  File "sub/foo.expected", line 1, characters 0-0:
+  --- sub/foo.expected
+  +++ sub/foo.output
+  @@ -0,0 +1 @@
+  +Inductive Corelib.Init.Datatypes.bool
+  [1]
+
+The test can also be run by name, like cram tests:
+
+  $ dune build @foo
+  File "sub/foo.expected", line 1, characters 0-0:
+  --- sub/foo.expected
+  +++ sub/foo.output
+  @@ -0,0 +1 @@
+  +Inductive Corelib.Init.Datatypes.bool
+  [1]
+
+And with a sub-directory too.
+
+  $ dune build @sub/foo
+  File "sub/foo.expected", line 1, characters 0-0:
+  --- sub/foo.expected
+  +++ sub/foo.output
+  @@ -0,0 +1 @@
+  +Inductive Corelib.Init.Datatypes.bool
+  [1]