refactor: update rocq extraction to use extracted_files instead of extracted_modules for version 0.13

Signed-off-by: Will Thomas <30wthomas@gmail.com>

Author: Durbatuluk1701

doc/rocq.rst

@@ -374,7 +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``: Support for ``extracted_files`` in ``rocq.extraction``.
+- ``0.13``: ``rocq.extraction`` now uses ``extracted_files`` instead of
+  ``extracted_modules``, supporting extraction to languages other than OCaml.
 
 .. _rocq-lang-1.0:
 
@@ -395,27 +396,38 @@ rocq.extraction
 Rocq may be instructed to *extract* sources as part of the compilation
 process by using the ``rocq.extraction`` stanza:
 
+For ``(rocq 0.12)`` and below:
+
 .. code:: dune
 
    (rocq.extraction
     (prelude <name>)
     (extracted_modules <names>)
+    <optional-fields>)
+
+For ``(rocq 0.13)`` and above:
+
+.. code:: dune
+
+   (rocq.extraction
+    (prelude <name>)
     (extracted_files <filenames>)
     <optional-fields>)
 
 - ``(prelude <name>)`` refers to the Rocq source that contains the extraction
   commands.
 
-- ``(extracted_modules <names>)`` is a list of OCaml modules extracted. For each
-  module name, Dune expects both a ``.ml`` and ``.mli`` file to be produced.
-
-- ``(extracted_files <filenames>)`` is a list of filenames (with extensions) that
-  will be produced by the extraction. This allows extraction to languages other
-  than OCaml, such as Haskell (``.hs``) or Scheme (``.scm``). Available since
-  ``(rocq 0.13)``.
-
-  At least one of ``extracted_modules`` or ``extracted_files`` must be specified.
-  Both can be provided simultaneously, and the targets will be merged.
+- ``(extracted_modules <names>)`` specifies the OCaml modules to be extracted.
+  For each module name, Dune expects both a ``.ml`` and ``.mli`` file to be
+  produced. Available in ``(rocq 0.12)`` and below; replaced by
+  ``extracted_files`` in ``(rocq 0.13)``.
+
+- ``(extracted_files <filenames>)`` is a list of filenames (with extensions)
+  that will be produced by the extraction. This allows extraction to languages
+  other than OCaml, such as Haskell (``.hs``) or Scheme (``.scm``). Available
+  since ``(rocq 0.13)``. Users upgrading from ``0.12`` should replace
+  ``(extracted_modules M1 ... Mn)`` with ``(extracted_files M1.ml M1.mli ... Mn.ml
+  Mn.mli)``.
 
 - ``<optional-fields>`` are ``flags``, ``stdlib``, ``theories``, and
   ``plugins``. All of these fields have the same meaning as in the

src/dune_rules/rocq/rocq_stanza.ml

@@ -70,52 +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
-    ; extracted_files : string list
+    { target_fnames : string list
     ; prelude : Loc.t * Rocq_module.Name.t
     ; buildable : Buildable.t
     }
 
-  let target_fnames t =
-    List.concat_map t.extracted_modules ~f:(fun m -> [ m ^ ".ml"; m ^ ".mli" ])
-    @ t.extracted_files
-  ;;
+  let target_fnames t = t.target_fnames
 
   let decode =
     fields
-      (let+ extracted_modules = field "extracted_modules" (repeat string) ~default:[]
-       and+ extracted_files =
-         field
+      (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)
-           ~default:[]
        and+ prelude = field "prelude" (located (string >>| Rocq_module.Name.make))
        and+ buildable = Buildable.decode
        and+ loc = loc in
-       if List.is_empty extracted_modules && List.is_empty extracted_files
-       then
-         User_error.raise
-           ~loc
-           [ Pp.text
-               "At least one of (extracted_modules) or (extracted_files) must be \
-                specified"
-           ];
-       let all_targets =
-         target_fnames { extracted_modules; extracted_files; prelude; buildable }
+       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
-       (match String.Map.of_list (List.map all_targets ~f:(fun t -> t, ())) with
-        | Ok _ -> ()
-        | Error (dup, (), ()) ->
-          User_warning.emit
-            ~loc
-            [ Pp.textf
-                "Duplicate target filename %S across (extracted_modules) and \
-                 (extracted_files)"
-                dup
-            ]);
-       { prelude; extracted_modules; extracted_files; buildable })
+       { target_fnames; prelude; buildable })
   ;;
 
   include Stanza.Make (struct

src/dune_rules/rocq/rocq_stanza.mli

@@ -27,8 +27,7 @@ end
 
 module Extraction : sig
   type t =
-    { extracted_modules : string list
-    ; extracted_files : string list
+    { target_fnames : string list
     ; prelude : Loc.t * Rocq_module.Name.t
     ; buildable : Buildable.t
     }

test/blackbox-tests/test-cases/rocq/extraction/extracted-files.t

@@ -1,4 +1,4 @@
-Test error when neither extracted_modules nor extracted_files is provided:
+Test error when extracted_files is not provided in rocq 0.13:
 
   $ cat >dune-project <<EOF
   > (lang dune 3.22)
@@ -21,8 +21,7 @@ Test error when neither extracted_modules nor extracted_files is provided:
   File "dune", lines 1-2, characters 0-33:
   1 | (rocq.extraction
   2 |  (prelude extr))
-  Error: At least one of (extracted_modules) or (extracted_files) must be
-  specified
+  Error: Field "extracted_files" is required
   [1]
 
 Test version gating: extracted_files requires (rocq 0.13):
@@ -47,7 +46,7 @@ Test version gating: extracted_files requires (rocq 0.13):
   0.13).
   [1]
 
-Test warning on duplicate target filename across extracted_modules and extracted_files:
+Test that extracted_modules is deleted in rocq 0.13 with a helpful error message:
 
   $ cat >dune-project <<EOF
   > (lang dune 3.22)
@@ -58,54 +57,16 @@ Test warning on duplicate target filename across extracted_modules and extracted
   > (rocq.extraction
   >  (prelude extr)
   >  (extracted_modules extr)
-  >  (extracted_files extr.ml)
   >  (flags (:standard -w -extraction-default-directory)))
   > EOF
 
   $ dune build
-  File "dune", lines 1-5, characters 0-140:
-  1 | (rocq.extraction
-  2 |  (prelude extr)
-  3 |  (extracted_modules extr)
-  4 |  (extracted_files extr.ml)
-  5 |  (flags (:standard -w -extraction-default-directory)))
-  Warning: Duplicate target filename "extr.ml" across (extracted_modules) and
-  (extracted_files)
-  $ ls _build/default | sort
-  Datatypes.ml
-  Datatypes.mli
-  extr.glob
-  extr.ml
-  extr.mli
-  extr.v
-  extr.vo
-  extr.vok
-  extr.vos
-
-Test completeness of both extracted_modules and extracted_files (expected failure):
-
-  $ cat >dune-project <<EOF
-  > (lang dune 3.22)
-  > (using rocq 0.13)
-  > EOF
-
-  $ cat >dune <<EOF
-  > (rocq.extraction
-  >  (prelude extr)
-  >  (extracted_modules extr)
-  >  (extracted_files fake.hs)
-  >  (flags (:standard -w -extraction-default-directory)))
-  > EOF
-
-  $ dune build
-  File "dune", lines 1-5, characters 0-140:
-  1 | (rocq.extraction
-  2 |  (prelude extr)
+  File "dune", line 3, characters 1-25:
   3 |  (extracted_modules extr)
-  4 |  (extracted_files fake.hs)
-  5 |  (flags (:standard -w -extraction-default-directory)))
-  Error: Rule failed to generate the following targets:
-  - fake.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 explicit filenames:
@@ -138,7 +99,7 @@ Test using extracted_files with explicit filenames:
   _build/default/Datatypes.ml
   _build/default/extr.ml
 
-Test using extracted_modules with Haskell outputs (expected failure):
+Test that extracted_modules in 0.13 gives deleted_in error for Haskell extraction:
 
   $ cat >dune-project <<EOF
   > (lang dune 3.22)
@@ -165,16 +126,12 @@ Test using extracted_modules with Haskell outputs (expected failure):
   > EOF
 
   $ dune build
-  File "dune", lines 1-4, characters 0-129:
-  1 | (rocq.extraction
-  2 |  (prelude extr)
+  File "dune", line 3, characters 1-41:
   3 |  (extracted_modules Datatypes.hs extr.hs)
-  4 |  (flags (:standard -w -extraction-default-directory)))
-  Error: Rule failed to generate the following targets:
-  - Datatypes.hs.ml
-  - Datatypes.hs.mli
-  - extr.hs.ml
-  - extr.hs.mli
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  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):
@@ -210,8 +167,6 @@ Test using extracted_files with Haskell outputs (expected success):
   extr.hs
   extr.v
   extr.vo
-  extr.vok
-  extr.vos
 
 Test rebuild does not clean extracted files:
 (NOTE: re-using above pre-built context)
@@ -223,7 +178,7 @@ Test rebuild does not clean extracted files:
   extr.v
   extr.vo
 
-Test using extracted_modules with Scheme outputs (expected failure):
+Test that extracted_modules in 0.13 gives deleted_in error for Scheme extraction:
 
   $ cat >dune-project <<EOF
   > (lang dune 3.22)
@@ -250,14 +205,12 @@ Test using extracted_modules with Scheme outputs (expected failure):
   > EOF
 
   $ dune build
-  File "dune", lines 1-4, characters 0-115:
-  1 | (rocq.extraction
-  2 |  (prelude extr)
+  File "dune", line 3, characters 1-27:
   3 |  (extracted_modules nb.scm)
-  4 |  (flags (:standard -w -extraction-default-directory)))
-  Error: Rule failed to generate the following targets:
-  - nb.scm.ml
-  - nb.scm.mli
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^
+  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):
@@ -291,6 +244,4 @@ Test using extracted_files with Scheme outputs (expected success):
   extr.glob
   extr.v
   extr.vo
-  extr.vok
-  extr.vos
   nb.scm