Adding extracted_files field to rocq.extraction stanza (#13997)

This PR adds an `extracted_files` field to the `rocq.extraction` stanza.
In particular, this field is used to specify files that should be
produced by extraction *other than* those purely meant for OCaml
extraction (the current `extracted_modules` field behavior).

The primary motivation for this is the following behavior: given a Rocq
extraction prelude `X.v` that extracts to Haskell and produces a file
`X.hs`, a single `dune build` will produce this file, but subsequent
`dune build` will wipe the `X.hs` from `_build/...`.

This behavior is mitigated by this PR and specifically witnessed by the
`Test rebuild does not clean extracted files:` test in
`test/blackbox-tests/test-cases/rocq/extraction/extracted-files.t`

---------

It is my belief that the `extracted_files` stanza could subsume
`extracted_modules`: `(extracted_modules F1 ... FN) --> (extracted_files
F1.ml F1.mli ... FN.ml FN.mli)`, however for compatibility I did not do
this, although maybe it is worth discussing.

Author: Alizter

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).

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 <name>)
-    (extracted_modules <names>)
+    (extracted_files <filenames>)
     <optional-fields>)
 
 - ``(prelude <name>)`` refers to the Rocq source that contains the extraction
   commands.
 
-- ``(extracted_modules <names>)`` is an exhaustive list of OCaml modules
-  extracted.
+- ``(extracted_files <filenames>)`` 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 <names>)`` 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)``.
 
 - ``<optional-fields>`` are ``flags``, ``stdlib``, ``theories``, and
   ``plugins``. All of these fields have the same meaning as in the

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

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

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

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