Stream: Dune devs & users

Topic: Several extraction in same dune file


view this post on Zulip Karl Palmskog (Jun 24 2023 at 14:55):

Consider the following dune-project:

(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 this Coq file Extr1.v:

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

And this 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, I get the following error:

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

Is this a bug or just a change done to the meaning of coq.extraction? Shouldn't this kind of breaking change be reserved for Coq-Dune version changes?

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 16:21):

IIRC theory.d is the suffix used by per-theory coqdep — maybe both stanzas generating a theory with the same logical path, and that stopped working because of the coqdep changes?

view this post on Zulip Karl Palmskog (Jun 24 2023 at 16:26):

the Coq version is held constant in my tests:

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 16:31):

I’m hinting at a dune change not a Coq change

view this post on Zulip Karl Palmskog (Jun 24 2023 at 16:33):

OK. It seems a huge hassle to have to have different directories just to extract a few different modules from different Coq theories...

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 16:33):

Indeed, from the 3.7.0 changelog:

coqdep is now called once per theory, instead of one time per Coq
file. This should significantly speed up some builds, as coqdep
startup time is often heavy (#7048, @Alizter, @ejgallego)

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 16:34):

The .theory.d file was just not generated before, so this change probably caused this bug

view this post on Zulip Karl Palmskog (Jun 24 2023 at 16:35):

seems plausible that this could be a consequence of coqdep treatment. If someone from dev team (Ali, Emilio, ...) gives green light I will report as issue, and propose the coqdep explanation

view this post on Zulip Ali Caglayan (Jun 24 2023 at 19:13):

Yeah it xomes from using a dummy theory name in extraction so the coqdep call creates DuneExtraction.theory.d in both cases. We should probably just use the name of the prelude in there somewhere. Please open an issue.

view this post on Zulip Karl Palmskog (Jun 24 2023 at 19:25):

https://github.com/ocaml/dune/issues/8042


Last updated: May 25 2024 at 21:01 UTC