Fixes #10739: anomaly with Extraction within a module

[herbelin]

When inside a module, module type or functor, we do as if we had first closed the module, module type or functor before asking to extract.

This implies a small change of behavior of Recursive Extraction in a module when none of the extracted term was referring to the outside of the module: the result is now encapsulated in the given module (this changes e.g. the test for #14100). On the other side, the new behavior makes Recursive Extraction also working in the presence of references outside the module.

Fixes #10739

Incidentally, it now also supports the example in #10796.

• Added / updated test-suite.
• Added changelog.

[SkySkimmer]

anomaly with

Require Extraction.

Module Type T.
  Definition foo := 0.
  Extraction foo.

[herbelin]

@SkySkimmer: well spotted, thanks, fixed.

[SkySkimmer]

What does it do on #17395 ?

[herbelin]

Sorry, my previous response was not properly answering the question (then deleting it). See #17395 for an answer. (In particular, there is no relation between #17395 and extracting within a module type, iianm.)

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[herbelin]

As far as I remember, this was ready. Maybe @ppedrot would have some time to look at it. Basically, when inside a module, module type or functor, the PR extracts as if we had first closed the module, and the code for warning when extracting from an open module or functor, or failing when extracting from an open module type are removed.

@coqbot: run full CI

[SkySkimmer]

Maybe we should make this an output test to make sure it doesn't produce garbage?

[herbelin]

Yes, that's worth. Done.

[coqbot-app]

🔴 CI failure at commit c3233a6 without any failure in the test-suite

✔️ Corresponding job for the base commit 6f1588d succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-geocoq

• You can also pass me a specific list of targets to minimize as arguments.

[herbelin]

@coqbot: run full CI

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[herbelin]

Looks ready.

[gares]

@SkySkimmer would you mind reviewing and eventually merging this one? It seems ready for 8.18

[SkySkimmer]

Seems to work

[SkySkimmer]

@coqbot merge now

[SkySkimmer]

This is generating files like test-suite/datatypes.ml
Should we gitignore them or is there something better we can do?

[herbelin]

With #16126 or #17392, it could be redirected to say /tmp... ?

Alternatively, a Separate Extraction TestCompile command could be provided... ?