diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 3d066fa2cb1..e3d4fe3f713 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/src/dune_rules/rocq/rocq_rules.ml @@ -820,7 +820,11 @@ 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 @@ -828,6 +832,14 @@ let setup_output_diff_rule ~loc ~dir ~sctx ~rocq_lang_version ~rocq_sources rocq (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 diff --git a/test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t b/test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t new file mode 100644 index 00000000000..002c7e7c956 --- /dev/null +++ b/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 < (include_subdirs qualified) + > (rocq.theory + > (name a)) + > EOF + + $ mkdir sub + $ cat > sub/foo.v < 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]