From 3c6aff42213f6a41321ac0ee7118dd5f9d425158 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 26 Jun 2026 21:41:27 +0200 Subject: [PATCH 1/2] Attach Rocq output tests to the right directory. Tests used to be attached to the runtest alias of the top-level directory of the rocq.theory stanza, even if they lived in some sub-directory via (include_subdirs qualified). Signed-off-by: Rodolphe Lepigre --- src/dune_rules/rocq/rocq_rules.ml | 3 +- .../test-cases/rocq/rocq-expected-alias.t | 40 +++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 3d066fa2cb1..251ac040bbb 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/src/dune_rules/rocq/rocq_rules.ml @@ -820,7 +820,8 @@ 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 alias = Alias.make ~dir:alias_dir Alias0.runtest in Simple_rules.Alias_rules.add sctx ~loc 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..ed4d9a847f2 --- /dev/null +++ b/test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t @@ -0,0 +1,40 @@ +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] + +But 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] + + From 1b320a827c66060d9fd82c96b2ec9e5b810bb977 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 26 Jun 2026 22:20:51 +0200 Subject: [PATCH 2/2] Allow using Rocq output test name as alias This is similar to what already exists with cram tests. Signed-off-by: Rodolphe Lepigre --- src/dune_rules/rocq/rocq_rules.ml | 13 +++++++++++- .../test-cases/rocq/rocq-expected-alias.t | 20 ++++++++++++++++++- 2 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 251ac040bbb..e3d4fe3f713 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/src/dune_rules/rocq/rocq_rules.ml @@ -821,7 +821,10 @@ let setup_output_diff_rule ~loc ~dir ~sctx ~rocq_lang_version ~rocq_sources rocq } in let alias_dir = Path.Build.parent_exn expected in - let alias = Alias.make ~dir:alias_dir Alias0.runtest 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 @@ -829,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 index ed4d9a847f2..002c7e7c956 100644 --- a/test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t +++ b/test/blackbox-tests/test-cases/rocq/rocq-expected-alias.t @@ -27,7 +27,7 @@ This has always worked: +Inductive Corelib.Init.Datatypes.bool [1] -But this used to fail: +And this used to fail: $ dune runtest sub File "sub/foo.expected", line 1, characters 0-0: @@ -37,4 +37,22 @@ But this used to fail: +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]