Adapt with respect to rocq-prover/rocq#21098

[tabareau]

No description provided.

[ppedrot]

Please merge now.

[jdchristensen]

@tabareau @ppedrot @SkySkimmer This has broken the Coq-HoTT CI (we still support 8.19), and was merged without any discussion. Also, as often happens, there is no explanation in the PR of why the change is being done or what it achieves.

[jdchristensen]

Here's a clickable link to the Rocq PR: rocq-prover/rocq#21098

[tabareau]

@jdchristensen we are sorry, we didn't know that the master branch of HoTT was supposed to compile on other version than rocq/master.

[tabareau]

We will try to do a backward compatible change instead.

[jdchristensen]

We plan to make 9.0 the minimum soon, so if you can find a fix that works for 9.0 and up, that would probably be good enough. I'm also hoping that we can make it so that rewriting uses our transport operation up to definitional equality.

[tabareau]

Hi @jdchristensen, you can revert the PR, I will do a new one that is backward compatible with a modification of PR#21098. However, the new mechanism implemented in PR#21098 for rewriting cannot be used in a backward compatible way for Coq-HoTT as the current code explicitly exposes the existence of internal_rew_... that no longer exists with the new mechanism. Maybe you should revisit your development process as having the same branch for benefiting from new Rocq features and being at the same time backward compatible with older version is fundamentally not possible. Such a process forces you to benefit from new features of the oldest supported version only.

[tabareau]

Note that the problem will be even more present with the introduction of algebraic universes that we plan to provide soon as you will not be able to use this mechanism in a backward compatible way. For this, you will really have to do a dedicated development branch or give up the backward compatibility.

[jdchristensen]

@tabareau We generally only keep backward compatibilty for one or two Rocq/Coq versions, aiming to give library users and developers a window of 6 months to a year before they need to upgrade. It's ok if we are delayed slightly in getting access to the latest Rocq features. Our current support of 8.19 is just due to inertia, not policy, which is why we'd be fine supporting only 9.0 and up at this point.

[jdchristensen]

@tabareau It looks like you might be doing the revert now? If so, I'll wait.

[jdchristensen]

the current code explicitly exposes the existence of internal_rew_... that no longer exists with the new mechanism.

I don't think we use this anywhere. The tactic and the test that mention these can be removed, I believe.