Remove dynamic scheme generation

[SkySkimmer]

No description provided.

[SkySkimmer]

@JasonGross @Janno @Alizter @jdchristensen @RalfJung @robbertkrebbers @gares @proux01
@benediktahrens @m-lindgren @nmvdw @rmatthes @mattam82 @yforster
please ensure your developments compile with warning missing-scheme set as error

[proux01]

@SkySkimmer for oddorder, I tried this math-comp/odd-order#84 which works well on this PR but fails on 9.1: math-comp/odd-order#84 What am I expected to do ? At worst I'm fine droping 9.1 support but Rocq compat policy is "compatibility with two successive versions" so I'd expect a solution working for both 9.1 and 9.2.

[SkySkimmer]

Maybe it's too early to remove this then

[RalfJung]

please ensure your developments compile with warning missing-scheme set as error

When I tried this around the 9.2 release, it was impossible because the new commands we have to use do not exist in Rocq 9.1. So, basically what @proux01 said -- I think this needs to wait a cycle.

[proux01]

So, let's complete this just after 9.3.0 is out I guess.

[RalfJung]

(Also FWIW the error messages this generates are pretty hard to interpret. It talks about Missing "rew_r" scheme, which apparently is related to Scheme Rewriting, but I have no idea how I am supposed to figure that out. I was not even able to find a list of valid schemes in the docs and there are no search results for rew_r.)

[SkySkimmer]

You can figure it out because the error tells you to use Scheme Rewriting.

[RalfJung]

Hm, in the CI log here I only see

File "./iris/bi/sbi_unfold.v", line 281, characters 7-21:
Error:
Missing "rew_r" scheme for TCEq.

[SkySkimmer]

You're looking at the error summary, it only contains the first line of the error. Also it's not guaranteed to be complete.

[RalfJung]

Ah right, locally I get more context. A bit unfortunate that CI swallows that, but maybe us project maintainers are not expected to look at that output.^^

[SkySkimmer]

The CI doesn't swallow it, just look back up in the log https://gitlab.inria.fr/coq/coq/-/jobs/7531633#L7658

[JasonGross]

Can the changelog get a description of adjustment that is needed?