Adapt to https://github.com/coq/coq/pull/19530

[proux01]

Adapt to coq/coq#19530
This should be backward compatible and can be merged at your convenience, before the upstream PR.

[xavierleroy]

Thanks for letting me know about coq/coq#19530 and for the proposed patch.

I'm curious: why does moving coq-stdlib to a separate repo should change anything to existing proofs? Does the move include changes to the theory files themselves? Should I expect more breakage like this from the move?

[proux01]

Sorry, this was a bit short on the explanations side. It's a bit technical though.
Tl;dr: the change should otherwise be mostly transparent.

In the process of giving the Stdlib its own repository, we chose, among other things, to keep the specification of primitive types (int63, float, permanent arrays and now strings) in the coq repo (since the primitive types have reduction rules implemented in the kernel, these are specifications of the kernel and it would be strange to export them in a library repo). It appears the float specification was using the old Zeq_bool instead of the newer Z.eqb. To avoid keeping also Zeq_bool in Coq repo just for that use, I made the update, hence the current pull request.

Other than that, Compcert is green in the CI in coq/coq#19530 and we chose to keep the dependency to coq-stdlib in the coq metapackage, so the change should be fairly transparent to users. There will be a new warning recommending the use of the From Stdlib Require form rather than just Require for Stdlib modules but as usual we will keep the compatibility for a few versions (I'd expect a few years in this case).

[xavierleroy]

OK, thanks for the extra explanations. I understand this is related to Zeq_bool and how it is used in Flocq (both in the original Flocq sources and in the version that is vendored inside CompCert). CompCert doesn't use Zeq_bool otherwise.

I'm OK in principle with this PR, but I'll wait a bit to see how @silene decides to go about it, i.e. work around the Zeq_bool issues as in https://gitlab.inria.fr/flocq/flocq/-/merge_requests/24, or switch entirely to Z.eqb.

[xavierleroy]

Also, after reading the CEP, I'm strongly in favor of keeping all of coq-stdlib in one package. The configure script for CompCert likes to check for Coq versions that have been tested successfully against CompCert. Probably this check will have to be extended to also check for coq-stdlib versions, hoping there is an easy way to find the version number for an installed coq-stdlib, even if not installed through OPAM. Checking for N versions of N sub-packages would be too much.

[proux01]

I'm OK in principle with this PR, but I'll wait a bit to see how @silene decides to go about it, i.e. work around the Zeq_bool issues as in https://gitlab.inria.fr/flocq/flocq/-/merge_requests/24, or switch entirely to Z.eqb.

FYI https://gitlab.inria.fr/flocq/flocq/-/merge_requests/24 is now merged. May I also emphasize that this is backward compatible, so I don't see much reason left not to merge.

Also, after reading the CEP, I'm strongly in favor of keeping all of coq-stdlib in one package. [...] Checking for N versions of N sub-packages would be too much.

I agree, note that (although it may be a bit buried into the details of the CEP) distributing diferent versions of each subpackage has never been even envisioned. Anyway, the subpackage point didn't get full consensus, so it's just not happening.

[silene]

work around the Zeq_bool issues or switch entirely to Z.eqb.

At some point, I will switch to Z.eqb. But since it is not convertible to Zeq_bool (for better or worse), I am reluctant to perform this change right now, for compatibility reasons.

[proux01]

@xavierleroy could this please be merged, this remains one of the last unmerged overlay of the upstream pull request

[xavierleroy]

OK, I caved under pressure. But I'm grumpy because I still don't understand the problem that needs to be solved here.