Having several Coq extraction stanzas leads to multiple rule error from Dune 3.7

[palmskog]

Expected Behavior

When I declare several coq.extraction stanzas in a single dune file producing different OCaml modules in Dune 3.7 and later, I expect dune build to work, as it did in (at least) Dune 3.5 and 3.6.

Actual Behavior

After running dune build I get a "multiple rule" error, like the following:

Error: Multiple rules generated for _build/default/DuneExtraction.theory.d:
- dune:1
- dune:5

Reproduction

Consider a minimal Coq extraction project which produces two modules, with the following dune-project file:

(lang dune 2.8)
(using coq 0.3)
(name extraction-multiple)

And the following dune file:

(coq.extraction
 (prelude Extr1)
 (extracted_modules Mod1)
)
(coq.extraction
 (prelude Extr2)
 (extracted_modules Mod2)
)

And the Coq file Extr1.v:

From Coq Require Import Extraction.
Extraction "Mod1.ml" app.

And the Coq file Extr2.v:

From Coq Require Import Extraction.
Extraction "Mod2.ml" length.

Up to and including Dune 3.6, this works fine with dune build. However, for Dune 3.7 and forward, including Dune 3.8.2, I get the following error:

$ dune build
Error: Multiple rules generated for _build/default/DuneExtraction.theory.d:
- dune:1
- dune:5

Specifications

• Version of dune (output of dune --version): 3.7.1
• Version of ocaml (output of ocamlc --version): 4.11.2
• Operating system (distribution and version): Ubuntu 22.04 LTS

Additional information

• This is independent of the Coq version used, the replication of the error for Dune 3.7.1 and 3.8.2 (and absence of error for 3.5.0 and 3.6.1) was done on Coq 8.15.1.
• The likely culprit is feature(coq): call coqdep once per theory #7048, as pointed out by @Blaisorblade.
• Producing several OCaml modules by extraction from the same dune file is a very convenient feature and if not supported, necessitates reorganizing some projects in an inconvenient way (lots of subdirectories).

This issue was invited for submission by @Alizter.

[Alizter]

As mentioned on zulip, the solution is to choose a better dummy theory name than DuneExtraction and use something from the name of the prelude probably.

[ejgallego]

Code is here:

dune/src/dune_rules/coq/coq_rules.ml

Lines 869 to 872 in 2a3ca31

	let setup_extraction_rules ~sctx ~dir ~dir_contents
	(s : Coq_stanza.Extraction.t) =
	let wrapper_name = "DuneExtraction" in
	let* coq_module =

So indeed, as @Alizter said, this should be pretty easy to fix, by generating a name that is more likely not to collide, or by letting the user specify it.

[palmskog]

I think it would make the most sense to just add the contents of prelude to "DuneExtraction", e.g.,

let wrapper_name = "DunExtraction" ^ prelude in

Personally, I don't really see a reason to be able to control this manually (maybe add that later if someone asks for it). And if I understand correctly, there is no point in having several coq.extraction stanzas with the same prelude (just add more modules to extracted_modules for the existing stanza).

[ejgallego]

Sounds good to me, we'll prepare a fix ASAP.