diff --git a/doc/rocq.rst b/doc/rocq.rst index 9a5f6f9bc96..58bab3513fb 100644 --- a/doc/rocq.rst +++ b/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`) 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,6 +373,7 @@ 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: @@ -379,7 +381,7 @@ 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` 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) diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 0f819c5cad2..d31fcd4db57 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/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 = diff --git a/src/dune_rules/rocq/rocq_sources.ml b/src/dune_rules/rocq/rocq_sources.ml index 2e85d1df3bf..eca4b625161 100644 --- a/src/dune_rules/rocq/rocq_sources.ml +++ b/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 = diff --git a/src/dune_rules/rocq/rocq_sources.mli b/src/dune_rules/rocq/rocq_sources.mli index 3c84572a118..288f1b742cb 100644 --- a/src/dune_rules/rocq/rocq_sources.mli +++ b/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 diff --git a/src/dune_rules/rocq/rocq_stanza.ml b/src/dune_rules/rocq/rocq_stanza.ml index 49c148b682c..6eeadcad495 100644 --- a/src/dune_rules/rocq/rocq_stanza.ml +++ b/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 diff --git a/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-root.t/run.t index e31fc1136a2..9c1c96ef365 100644 --- a/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-root.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/rocq/expected-modules.t b/test/blackbox-tests/test-cases/rocq/expected-modules.t index bd4a66bf6a8..04a206f5447 100644 --- a/test/blackbox-tests/test-cases/rocq/expected-modules.t +++ b/test/blackbox-tests/test-cases/rocq/expected-modules.t @@ -1,8 +1,8 @@ Test that expected files work with explicit (modules ...): $ cat > dune-project < (lang dune 3.21) - > (using rocq 0.11) + > (lang dune 3.22) + > (using rocq 0.12) > EOF $ cat > dune <dune-project < (lang dune 3.21) - > (using rocq 0.11) + > (lang dune 3.22) + > (using rocq 0.12) > EOF $ cat >extract.v < dune-project < (lang dune 3.21) - > (using rocq 0.11) + > (lang dune 3.22) + > (using rocq 0.12) > EOF $ cat > dune < dune-project < (lang dune 3.21) - > (using rocq 0.11) + > (lang dune 3.22) + > (using rocq 0.12) > EOF $ cat > dune <