Factor wrapper for extraction, use in dune rocq top.

Signed-off-by: Rodolphe Lepigre <rodolphe.lepigre@skylabs-ai.com>

Author: rlepigre-skylabs-ai

bin/rocq/rocqtop.ml

@@ -122,7 +122,7 @@ let term =
         | Some (`Extraction extr) ->
           ( Dune_rules.Rocq.Rocq_rules.rocqtop_args_extraction ~sctx ~dir extr rocq_module
           , extr.buildable.use_stdlib
-          , "DuneExtraction"
+          , Dune_rules.Rocq.Rocq_rules.extraction_wrapper_name extr
           , extr.buildable.mode )
       in
       (* Run rocqdep *)

src/dune_rules/rocq/rocq_rules.ml

@@ -1245,8 +1245,11 @@ let setup_rocqpp_rules ~sctx ~dir ({ loc; modules } : Rocq_stanza.Rocqpp.t) =
   List.rev_map ~f:mlg_rule mlg_files |> Super_context.add_rules ~loc ~dir sctx
 ;;
 
+let extraction_wrapper_name (s : Rocq_stanza.Extraction.t) : string =
+  "Dune_Extraction_" ^ Rocq_module.Name.to_string (snd s.prelude)
+
 let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction.t) =
-  let wrapper_name = "DuneExtraction" ^ Rocq_module.Name.to_string (snd s.prelude) in
+  let wrapper_name = extraction_wrapper_name s in
   let* rocq_module =
     let+ rocq = Dir_contents.rocq dir_contents in
     Rocq_sources.extract rocq s
@@ -1315,7 +1318,7 @@ let rocqtop_args_extraction ~sctx ~dir (s : Rocq_stanza.Extraction.t) rocq_modul
     let context = Super_context.context sctx |> Context.name in
     extraction_context ~context ~scope s.buildable
   in
-  let wrapper_name = "DuneExtraction" ^ Rocq_module.Name.to_string (snd s.prelude) in
+  let wrapper_name = extraction_wrapper_name s in
   let boot_type = Bootstrap.make ~scope ~use_stdlib ~wrapper_name rocq_module in
   let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in
   let per_file_flags = None in

src/dune_rules/rocq/rocq_rules.mli

@@ -23,6 +23,10 @@ val deps_of
   -> Rocq_module.t
   -> unit Dune_engine.Action_builder.t
 
+(** Wrapper name used for the extraction stanza, used for calling [deps_of] on
+    in `dune rocq top`. *)
+val extraction_wrapper_name : Rocq_stanza.Extraction.t -> string
+
 (** ** Rules for Rocq stanzas *)
 
 (** [rocq.theory] stanza rules *)

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

@@ -42,5 +42,5 @@
   Mod2.ml
   Mod2.mli
   $ ls _build/default/.*.d | sort
-  _build/default/.DuneExtractionExtr1.theory.d
-  _build/default/.DuneExtractionExtr2.theory.d
+  _build/default/.Dune_Extraction_Extr1.theory.d
+  _build/default/.Dune_Extraction_Extr2.theory.d

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

@@ -44,10 +44,10 @@
   $ ls _build/default
   Datatypes.ml
   Datatypes.mli
-  NDuneExtraction_extract.cmi
-  NDuneExtraction_extract.cmx
-  NDuneExtraction_extract.cmxs
-  NDuneExtraction_extract.o
+  NDune_Extraction_extract_extract.cmi
+  NDune_Extraction_extract_extract.cmx
+  NDune_Extraction_extract_extract.cmxs
+  NDune_Extraction_extract_extract.o
   extract.glob
   extract.ml
   extract.mli