separate synterp phase

[gares]

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]

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

[gares]

Ok

[gares]

@CohenCyril is this a bug in HB.structure?
The module MathCompCompatFoo is exported here, but not when one issues HB.reexport.
Is this intended?

[gares]

The snippet is outdated, but the question still valid.

[CohenCyril]

It looks like a bug indeed, I think it should be marked to be exported via HB.reexport

[gares]

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]

Please merge now