search

AbsInt / CompCert

The CompCert formally-verified C compiler
https://compcert.org
Other
1.88k stars 228 forks source link

Adapt w.r.t. coq/coq#19343. #515

Closed ppedrot closed 3 months ago

ppedrot commented 3 months ago

Should be backwards compatible.

xavierleroy commented 3 months ago

Thanks for the patch. It seems to be about extraction, while https://github.com/coq/coq/pull/19343 is about functional induction. Could you tell us more?

proux01 commented 3 months ago

coq/coq#19343 removes the dependency of stdlib's MSetAVL on FunInd which is itself requiring Extraction. It appears Compcert was relying on this transitive requirement, the current pull request just makes that requirement explicit.

xavierleroy commented 3 months ago

Crystal clear! Thanks for the explanation.

xavierleroy commented 3 months ago

I think that in the long run Menhir itself should generate the Require Extraction directive. https://gitlab.inria.fr/fpottier/menhir/-/issues/75