search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

separate synterp phase #406

Closed gares closed 8 months ago

gares commented 9 months ago

Since Coq 8.18 the parsing (synterp) phase of commands must be separate from the execution one (interp). The synterp phase must declare operations on module and section (and notations, be we don't have them).

Only Coq-Elpi 2.0 has (will have) support for this feature. See LPCIC/coq-elpi#557

This PR fixes HB when used with Vscoq2. This PR removes the code of HB.lock and rebinds elpi.apps.locker(mlock) to that name.

CohenCyril commented 9 months ago

I think the removal of HB.lock will break mathcomp. Maybe we could make a deprecated alias to mlock

gares commented 9 months ago

Ok

gares commented 9 months ago

I think this PR is ready now, although still blocked by the release of coq-elpi 2.0. And the coq-master job also needs an update to the coq-master branch in Coq-Elpi which happens after the release.

I'm dropping 8.17 support. The only problem is that now the two phases need to be in sync, and we do generate random module names. Coq-Elpi 2 has a commodity API which lets one randomize the name at synterp time, and just reuse the same name at interp time. This choice is debatable, but at the same this PR should be 100% backward compatible. I mean, on 8.17 we can use the last release of HB. This compatibility drop is only annoying if we add to HB new features and use them in MC.

SkySkimmer commented 8 months ago

Please merge now