Guard Rocq output test on (lang rocq 0.12).

doc/rocq.rst

@@ -44,7 +44,7 @@ example, adding
 
 .. code:: dune
 
-    (using rocq 0.11)
+    (using rocq 0.12)
 
 to a :doc:`/reference/dune-project/index` file enables using the
 ``rocq.theory`` stanza and other ``rocq.*`` stanzas. See the :ref:`Dune Rocq
@@ -85,6 +85,7 @@ When a ``.v`` file has a corresponding ``.expected`` file, Rocq's standard
 output is captured instead of being output to the terminal, and the output is
 diffed with the ``.expected`` file as part of the ``runtest`` alias. When the
 output differs, it can be promoted as with, e.g., cram tests.
+(Appeared in :ref:`Coq lang 0.12<rocq-lang>`)
 
 For usage of this stanza, see the :ref:`rocq-examples`.
 
@@ -363,7 +364,7 @@ The Rocq lang can be modified by adding the following to a
 
 .. code:: dune
 
-    (using rocq 0.11)
+    (using rocq 0.12)
 
 The supported Rocq language versions (not the version of Rocq) are:
 
@@ -372,14 +373,15 @@ The supported Rocq language versions (not the version of Rocq) are:
   + Dune won't install .cmxs files in user-contrib (along .vo files) anymore.
   + ``(mode native)`` is not allowed anymore. It is the default if Rocq was configured with native compute enabled.
   + ``COQPATH`` is not recognized anymore, use ``ROCQPATH``.
+- ``0.12``: Support for output tests.
 
 .. _rocq-lang-1.0:
 
 Rocq Language Version 1.0
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Guarantees with respect to stability are not yet provided, but we
-intend that the ``(0.11)`` version of the language becomes ``1.0``.
+intend that the ``(0.12)`` version of the language becomes ``1.0``.
 The ``1.0`` version of Rocq lang will commit to a stable set of
 functionality. All the features below are expected to reach ``1.0``
 unchanged or minimally modified.
@@ -456,7 +458,7 @@ lang<rocq-lang>` stanza present:
 .. code:: dune
 
   (lang dune 3.22)
-  (using rocq 0.11)
+  (using rocq 0.12)
 
 Next we need a :doc:`/reference/dune/index` file with a :ref:`rocq-theory`
 stanza:
@@ -687,7 +689,7 @@ the plugin to sit in, otherwise Rocq will not be able to find it.
 .. code:: dune
 
   (lang dune 3.22)
-  (using rocq 0.11)
+  (using rocq 0.12)
 
   (package
    (name my-rocq-plugin)

src/dune_rules/rocq/rocq_rules.ml

@@ -799,8 +799,8 @@ module Per_file = struct
   ;;
 end
 
-let setup_output_diff_rule ~loc ~dir ~sctx ~rocq_sources rocq_module =
-  match Rocq_sources.expected_file rocq_sources rocq_module with
+let setup_output_diff_rule ~loc ~dir ~sctx ~rocq_lang_version ~rocq_sources rocq_module =
+  match Rocq_sources.expected_file ~rocq_lang_version rocq_sources rocq_module with
   | None -> Memo.return ()
   | Some expected ->
     let output = Rocq_module.output_file ~obj_dir:dir rocq_module in
@@ -825,6 +825,7 @@ let setup_rocqc_rule
       ~rocqc_dir
       ~file_targets
       ~stanza_flags
+      ~rocq_lang_version
       ~modules_flags
       ~theories_deps
       ~mode
@@ -851,8 +852,9 @@ let setup_rocqc_rule
     |> List.map ~f:fst
   in
   let output_file =
-    Option.map (Rocq_sources.expected_file rocq_sources rocq_module) ~f:(fun _ ->
-      Rocq_module.output_file ~obj_dir:dir rocq_module)
+    Option.map
+      (Rocq_sources.expected_file ~rocq_lang_version rocq_sources rocq_module)
+      ~f:(fun _ -> Rocq_module.output_file ~obj_dir:dir rocq_module)
   in
   let targets =
     let targets = Option.to_list output_file @ obj_files in
@@ -1078,6 +1080,7 @@ let extraction_context ~context ~scope (buildable : Rocq_stanza.Buildable.t) =
 let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) =
   let* scope = Scope.DB.find_by_dir dir in
   let name = s.name in
+  let rocq_lang_version = s.buildable.rocq_lang_version in
   let theory, theories_deps, ml_flags, mlpack_rule =
     let context = Super_context.context sctx |> Context.name in
     theory_context ~context ~scope ~name s.buildable
@@ -1151,6 +1154,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) =
       ~sctx
       ~file_targets:[]
       ~stanza_flags
+      ~rocq_lang_version
       ~modules_flags
       ~rocqc_dir
       ~theories_deps
@@ -1161,7 +1165,13 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) =
       ~theory_dirs
       ~rocq_sources:rocq_dir_contents
       rocq_module
-    >>> setup_output_diff_rule ~loc ~dir ~sctx ~rocq_sources:rocq_dir_contents rocq_module)
+    >>> setup_output_diff_rule
+          ~loc
+          ~dir
+          ~sctx
+          ~rocq_lang_version
+          ~rocq_sources:rocq_dir_contents
+          rocq_module)
   (* And finally the rocqdoc rules *)
   >>> setup_rocqdoc_rules ~sctx ~dir ~theories_deps s rocq_modules
 ;;
@@ -1286,6 +1296,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction.
   in
   let loc = s.buildable.loc in
   let use_stdlib = s.buildable.use_stdlib in
+  let rocq_lang_version = s.buildable.rocq_lang_version in
   let* scope = Scope.DB.find_by_dir dir in
   let theories_deps, ml_flags, mlpack_rule =
     let context = Super_context.context sctx |> Context.name in
@@ -1324,6 +1335,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction.
         ~scope
         ~file_targets
         ~stanza_flags:s.buildable.flags
+        ~rocq_lang_version
         ~modules_flags
         ~sctx
         ~loc
@@ -1337,7 +1349,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction.
         ~ml_flags
         ~theory_dirs:Path.Build.Set.empty
         ~rocq_sources
-  >>> setup_output_diff_rule ~loc ~dir ~sctx ~rocq_sources rocq_module
+  >>> setup_output_diff_rule ~loc ~dir ~sctx ~rocq_lang_version ~rocq_sources rocq_module
 ;;
 
 let rocqtop_args_extraction ~sctx ~dir (s : Rocq_stanza.Extraction.t) rocq_module =

src/dune_rules/rocq/rocq_sources.ml

@@ -140,11 +140,14 @@ let of_dir stanzas ~dir ~include_subdirs ~dirs =
 
 let lookup_module t m = Rocq_module.Map.find t.rev_map m
 
-let expected_file t m =
-  let source = Rocq_module.source m in
-  match Path.as_in_build_dir source with
-  | Some source -> Path.Build.Map.find t.expected_files source
-  | None -> None
+let expected_file ~rocq_lang_version t m =
+  if rocq_lang_version >= (0, 12)
+  then (
+    let source = Rocq_module.source m in
+    match Path.as_in_build_dir source with
+    | Some source -> Path.Build.Map.find t.expected_files source
+    | None -> None)
+  else None
 ;;
 
 let mlg_files ~sctx ~dir ~modules =

src/dune_rules/rocq/rocq_sources.mli

@@ -43,7 +43,11 @@ val lookup_module
   -> [ `Theory of Theory.t | `Extraction of Extraction.t ] option
 
 (** Returns the path to the .expected file for a module, if one exists *)
-val expected_file : t -> Rocq_module.t -> Path.Build.t option
+val expected_file
+  :  rocq_lang_version:Dune_sexp.Syntax.Version.t
+  -> t
+  -> Rocq_module.t
+  -> Path.Build.t option
 
 val mlg_files
   :  sctx:Super_context.t

src/dune_rules/rocq/rocq_stanza.ml

@@ -18,7 +18,7 @@ let rocq_syntax =
   Dune_lang.Syntax.create
     ~name:(Syntax.Name.parse "rocq")
     ~desc:"Rocq Prover build language"
-    [ (0, 11), `Since (3, 21) ]
+    [ (0, 11), `Since (3, 21); (0, 12), `Since (3, 22) ]
 ;;
 
 let get_rocq_syntax () = Dune_lang.Syntax.get_exn rocq_syntax

test/blackbox-tests/test-cases/rocq/coqtop/coqtop-root.t/run.t

@@ -21,6 +21,6 @@ This test is currently broken due to the workspace resolution being faulty #5899
   1 | (rocq.theory
   2 |  (name foo))
   Error: 'rocq.theory' is available only when rocq is enabled in the
-  dune-project or workspace file. You must enable it using (using rocq 0.11) in
+  dune-project or workspace file. You must enable it using (using rocq 0.12) in
   the file.
   [1]

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

@@ -1,8 +1,8 @@
 Test that expected files work with explicit (modules ...):
 
   $ cat > dune-project <<EOF
-  > (lang dune 3.21)
-  > (using rocq 0.11)
+  > (lang dune 3.22)
+  > (using rocq 0.12)
   > EOF
 
   $ cat > dune <<EOF

test/blackbox-tests/test-cases/rocq/extraction/extract.t

@@ -1,6 +1,6 @@
   $ cat >dune-project <<EOF
-  > (lang dune 3.21)
-  > (using rocq 0.11)
+  > (lang dune 3.22)
+  > (using rocq 0.12)
   > EOF
 
   $ cat >extract.v <<EOF

test/blackbox-tests/test-cases/rocq/github3624.t

@@ -17,6 +17,6 @@ good when the coq extension is not enabled.
   1 | (rocq.theory
   2 |  (name foo))
   Error: 'rocq.theory' is available only when rocq is enabled in the
-  dune-project or workspace file. You must enable it using (using rocq 0.11) in
+  dune-project or workspace file. You must enable it using (using rocq 0.12) in
   the file.
   [1]

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

@@ -1,8 +1,8 @@
 Testing the expected test support.
 
   $ cat > dune-project <<EOF
-  > (lang dune 3.21)
-  > (using rocq 0.11)
+  > (lang dune 3.22)
+  > (using rocq 0.12)
   > EOF
 
   $ cat > dune <<EOF

test/blackbox-tests/test-cases/rocq/rocq-native/coqtop/coqtop-root.t/run.t

@@ -22,6 +22,6 @@ This test is currently broken due to the workspace resolution being faulty #5899
   1 | (rocq.theory
   2 |  (name foo))
   Error: 'rocq.theory' is available only when rocq is enabled in the
-  dune-project or workspace file. You must enable it using (using rocq 0.11) in
+  dune-project or workspace file. You must enable it using (using rocq 0.12) in
   the file.
   [1]

test/blackbox-tests/test-cases/rocq/rocq-test-mode.t

@@ -1,8 +1,8 @@
 Testing the expected test support.
 
   $ cat > dune-project <<EOF
-  > (lang dune 3.21)
-  > (using rocq 0.11)
+  > (lang dune 3.22)
+  > (using rocq 0.12)
   > EOF
 
   $ cat > dune <<EOF