diff --git a/doc/changes/added/13997.md b/doc/changes/added/13997.md new file mode 100644 index 00000000000..50521bda990 --- /dev/null +++ b/doc/changes/added/13997.md @@ -0,0 +1,3 @@ +- `rocq.extraction`: Add `extracted_files` field in `(rocq 0.13)`, replacing + `extracted_modules`, supporting extraction to languages other than OCaml + (#13997, @Durbatuluk1701). diff --git a/doc/rocq.rst b/doc/rocq.rst index 4ba692b3703..622f4fdb2f0 100644 --- a/doc/rocq.rst +++ b/doc/rocq.rst @@ -374,6 +374,8 @@ The supported Rocq language versions (not the version of Rocq) are: + ``(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. +- ``0.13``: ``rocq.extraction`` now uses ``extracted_files`` instead of + ``extracted_modules``, supporting extraction to languages other than OCaml. .. _rocq-lang-1.0: @@ -391,21 +393,33 @@ unchanged or minimally modified. rocq.extraction --------------- -Rocq may be instructed to *extract* OCaml sources as part of the compilation +Rocq may be instructed to *extract* sources as part of the compilation process by using the ``rocq.extraction`` stanza: .. code:: dune (rocq.extraction (prelude ) - (extracted_modules ) + (extracted_files ) ) - ``(prelude )`` refers to the Rocq source that contains the extraction commands. -- ``(extracted_modules )`` is an exhaustive list of OCaml modules - extracted. +- ``(extracted_files )`` is the list of files Dune expects the + extraction to produce. Each entry is a filename with its extension, for + example OCaml (``.ml``, ``.mli``), Haskell (``.hs``), or Scheme (``.scm``). + + .. versionadded:: 3.23 + + +.. note:: + + ``(extracted_modules )`` is the predecessor to ``extracted_files``, + available in ``(rocq 0.12)`` and below. It accepts bare module names and + expects Dune to produce both a ``.ml`` and ``.mli`` file for each. Users + upgrading from ``0.12`` should replace ``(extracted_modules M1 ... Mn)`` + with ``(extracted_files M1.ml M1.mli ... Mn.ml Mn.mli)``. - ```` are ``flags``, ``stdlib``, ``theories``, and ``plugins``. All of these fields have the same meaning as in the diff --git a/src/dune_rules/dir_contents.ml b/src/dune_rules/dir_contents.ml index 59d32c91519..965f4126439 100644 --- a/src/dune_rules/dir_contents.ml +++ b/src/dune_rules/dir_contents.ml @@ -177,7 +177,7 @@ end = struct Path.Build.set_extension mlg_file ~ext:Filename.Extension.ml |> Path.Build.basename) | Rocq_stanza.Extraction.T s -> - Memo.return (Rocq_stanza.Extraction.ml_target_fnames s) + Memo.return (Rocq_stanza.Extraction.target_fnames s) | Rule_conf.T rule -> Simple_rules.user_rule sctx rule ~dir ~expander >>| (function diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 5b66af72120..12150c01848 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/src/dune_rules/rocq/rocq_rules.ml @@ -1297,7 +1297,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction. let* rocq_sources = Dir_contents.rocq dir_contents in let rocq_module = Rocq_sources.extract rocq_sources s in let file_targets = - Rocq_stanza.Extraction.ml_target_fnames s |> List.map ~f:(Path.Build.relative dir) + Rocq_stanza.Extraction.target_fnames s |> List.map ~f:(Path.Build.relative dir) in let loc = s.buildable.loc in let use_stdlib = s.buildable.use_stdlib in diff --git a/src/dune_rules/rocq/rocq_stanza.ml b/src/dune_rules/rocq/rocq_stanza.ml index 6eeadcad495..fc0ddb42198 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, 12), `Since (3, 22) ] + [ (0, 11), `Since (3, 21); (0, 12), `Since (3, 22); (0, 13), `Since (3, 23) ] ;; let get_rocq_syntax () = Dune_lang.Syntax.get_exn rocq_syntax @@ -70,23 +70,48 @@ end module Extraction = struct type t = - { (* not a list of modules because we want to preserve whatever case Rocq - uses *) - extracted_modules : string list + { target_fnames : string list ; prelude : Loc.t * Rocq_module.Name.t ; buildable : Buildable.t } - let ml_target_fnames t = - List.concat_map t.extracted_modules ~f:(fun m -> [ m ^ ".ml"; m ^ ".mli" ]) - ;; + let target_fnames t = t.target_fnames let decode = fields - (let+ extracted_modules = field "extracted_modules" (repeat string) + (let* ver = get_rocq_syntax () in + let+ extracted_modules_opt = + field_o + "extracted_modules" + (Dune_lang.Syntax.deleted_in + rocq_syntax + (0, 13) + ~extra_info: + "Use (extracted_files ...) instead, listing each .ml and .mli file \ + explicitly." + >>> repeat string) + and+ extracted_files_opt = + field_o + "extracted_files" + (Dune_lang.Syntax.since rocq_syntax (0, 13) >>> repeat string) and+ prelude = field "prelude" (located (string >>| Rocq_module.Name.make)) - and+ buildable = Buildable.decode in - { prelude; extracted_modules; buildable }) + and+ buildable = Buildable.decode + and+ loc = loc in + let target_fnames = + if ver < (0, 13) + then ( + match extracted_modules_opt with + | None -> + User_error.raise ~loc [ Pp.text "Field \"extracted_modules\" is required" ] + | Some modules -> + List.concat_map modules ~f:(fun m -> [ m ^ ".ml"; m ^ ".mli" ])) + else ( + match extracted_files_opt with + | None -> + User_error.raise ~loc [ Pp.text "Field \"extracted_files\" is required" ] + | Some files -> files) + in + { target_fnames; prelude; buildable }) ;; include Stanza.Make (struct diff --git a/src/dune_rules/rocq/rocq_stanza.mli b/src/dune_rules/rocq/rocq_stanza.mli index 106c5498944..98061a4f1ce 100644 --- a/src/dune_rules/rocq/rocq_stanza.mli +++ b/src/dune_rules/rocq/rocq_stanza.mli @@ -27,12 +27,12 @@ end module Extraction : sig type t = - { extracted_modules : string list + { target_fnames : string list ; prelude : Loc.t * Rocq_module.Name.t ; buildable : Buildable.t } - val ml_target_fnames : t -> string list + val target_fnames : t -> string list include Stanza.S with type t := t end diff --git a/test/blackbox-tests/test-cases/rocq/extraction/extracted-files.t b/test/blackbox-tests/test-cases/rocq/extraction/extracted-files.t new file mode 100644 index 00000000000..84fc122436b --- /dev/null +++ b/test/blackbox-tests/test-cases/rocq/extraction/extracted-files.t @@ -0,0 +1,270 @@ +Test error when extracted_files is not provided in rocq 0.13: + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb := true. + > Require Extraction. + > Extraction Language OCaml. + > Separate Extraction nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr)) + > EOF + + $ dune build + File "dune", lines 1-2, characters 0-33: + 1 | (rocq.extraction + 2 | (prelude extr)) + Error: Field "extracted_files" is required + [1] + +Test version gating: extracted_files requires (rocq 0.13 -> lang dune 3.23): + + $ cat >dune-project < (lang dune 3.22) + > (using rocq 0.13) + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_files foo.hs)) + > EOF + + $ dune build + File "dune-project", line 2, characters 12-16: + 2 | (using rocq 0.13) + ^^^^ + Error: Version 0.13 of Rocq Prover build language is not supported until + version 3.23 of the dune language. + Supported versions of this extension in version 3.22 of the dune language: + - 0.1 to 0.12 + [1] + +Test version gating: extracted_files requires (rocq 0.13): + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.12) + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_files foo.hs)) + > EOF + + $ dune build + File "dune", line 3, characters 1-25: + 3 | (extracted_files foo.hs)) + ^^^^^^^^^^^^^^^^^^^^^^^^ + Error: 'extracted_files' is only available since version 0.13 of Rocq Prover + build language. Please update your dune-project file to have (using rocq + 0.13). + [1] + +Test that extracted_modules is deleted in rocq 0.13 with a helpful error message: + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_modules extr) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + File "dune", line 3, characters 1-25: + 3 | (extracted_modules extr) + ^^^^^^^^^^^^^^^^^^^^^^^^ + Error: 'extracted_modules' was deleted in version 0.13 of Rocq Prover build + language. Use (extracted_files ...) instead, listing each .ml and .mli file + explicitly. + [1] + +Test using extracted_files with explicit filenames: + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Separate Extraction nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_files Datatypes.ml Datatypes.mli extr.ml extr.mli) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + $ ls _build/default/Datatypes.ml _build/default/extr.ml + _build/default/Datatypes.ml + _build/default/extr.ml + +Test that extracted_modules in 0.13 gives deleted_in error for Haskell extraction: + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Extraction Language Haskell. + > Separate Extraction nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_modules Datatypes.hs extr.hs) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + File "dune", line 3, characters 1-41: + 3 | (extracted_modules Datatypes.hs extr.hs) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + Error: 'extracted_modules' was deleted in version 0.13 of Rocq Prover build + language. Use (extracted_files ...) instead, listing each .ml and .mli file + explicitly. + [1] + +Test using extracted_files with Haskell outputs (expected success): + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Extraction Language Haskell. + > Separate Extraction nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_files Datatypes.hs extr.hs) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + $ ls _build/default | sort + Datatypes.hs + extr.glob + extr.hs + extr.v + extr.vo + +Test rebuild does not clean extracted files: +(NOTE: re-using above pre-built context) + $ dune build + $ ls _build/default | sort + Datatypes.hs + extr.glob + extr.hs + extr.v + extr.vo + +Test that extracted_modules in 0.13 gives deleted_in error for Scheme extraction: + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Extraction Language Scheme. + > Extraction "nb.scm" nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_modules nb.scm) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + File "dune", line 3, characters 1-27: + 3 | (extracted_modules nb.scm) + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + Error: 'extracted_modules' was deleted in version 0.13 of Rocq Prover build + language. Use (extracted_files ...) instead, listing each .ml and .mli file + explicitly. + [1] + +Test using extracted_files with Scheme outputs (expected success): + + $ cat >dune-project < (lang dune 3.23) + > (using rocq 0.13) + > EOF + + $ cat >extr.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Extraction Language Scheme. + > Extraction "nb.scm" nb. + > EOF + + $ cat >dune < (rocq.extraction + > (prelude extr) + > (extracted_files nb.scm) + > (flags (:standard -w -extraction-default-directory))) + > EOF + + $ dune build + $ ls _build/default | sort + extr.glob + extr.v + extr.vo + nb.scm