use Z.eqb_eq instead of Z.eqb_compare, fold Zeq_bool (for coq/coq#19801)

[andres-erbsen]

No description provided.

[xavierleroy]

I could use more explanations for this PR. From a distance, it looks like it reverts #524 (another PR that was forced upon me without much explanation) and goes in another direction.

What are the backward and forward compatibility objectives for the present PR?

[xavierleroy]

Lo and behold, this PR doesn't build with 8.17 nor with 8.20. There's no way I can consider this PR. Sorry.

[andres-erbsen]

Dear maintainer,

First, my apologies for missing that the existing compat wrapper was very recent and sending you a broken PR. In fact, it looks like reverting the previous PR might have been exactly what I needed to do.

The underlying technical problem here is that the duplication of duplication of Zeq_bool and Z.eqb is a common paper cut, both for user proofs and because it breaks ring morphisms for unsuspecting users who do Add Ring with Z.eqb while stdlib does it with Zeq_bool (or vice versa, if we were to switch stdlib over). I am just looking to clean up this duplication (which is itself a compat-dance mess from long ago), hopefully to never have to deal with Zeq_bool again. The other PR seems to have replaced some but not all uses of Zeq_bool with Z.eqb to clean up (the dependency list of) a part of stdlib, hence pushing the old compat dance out to new boundary that is crossed in this repository.

As for higher-level takeaways, I want to let you know that I see your pain, and I think it is entirely reasonable to want to understand any changes to your project. We clearly have to do better on the latter -- I do want to keep evolving and cleaning up stdlib, and doing so is only possible if we can adapt the projects that depend on stdlib. If we had more reviewers for stdlib changes, I'd suggest we review outgoing compat changes between ourselves first, and I will make a renewed effort to keep an eye out for them myself, but I cannot promise that it'll be exhaustive and catch all silliness. If you have other ideas for how this experience could be less frustrating for you, please let us know.

I have created #535 with what I think now may be a good way forward. Is there a way I can kick off the necessary builds and tests before requesting a review from you? (The modified file builds on 8.18 and master.)

Thank you for your patience with this.

[xavierleroy]

Thank you for the extra bits of context.

I'm all in favor of removing the duplication you mention and to use Z.eqb exclusively. Indeed, CompCert itself doesn't use Zeq_bool: it's only because CompCert depends on Flocq and Flocq uses Zeq_bool that CompCert gets involved in this duplication-removal project.

In #524 I suggested that it's Flocq that needs fixing to use Z.eqb throughout, but got a stern "no" from @silene (#524 (comment)). Has this changed? What are you @andres-erbsen going to do for Flocq?

[silene]

My answer was not meant to be understood as a "no"; on the contrary I was agreeing to it. I was just saying that I will not be releasing right now a version of Flocq that has lost compatibility with three versions of Coq at once. Nonetheless, I have merged the change in the repository, and it will be shipped once this abrupt loss of compatibility feels worth the cost.