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.