overlay for coq/coq#12162

Thanks for the MR.

While this fix is accurate for std++, I'm a bit concerned about the consequences for our reverse dependencies: le on nat is used so often that it's very annoying that the version of bool shadows the version on nat now.

Isn't there another fix by changing the order imports to make sure that we get the version on nat with the usual std++ imports?

The modification on numbers.v should mask Bool.le by Nat.le. Concerning sets.v, I made the lightest possible modifications, I do not know if adding some Require Import Peano. would strengthen things. I have tested the modified std++ with lambda-rust and perennial (since they belong to Coq CI) and it worked without any further modification.

This renaming will certainly have an impact on a number of developments but then it is a question about doing the modification in Coq's standard library or not at all. Do you have something else in mind? By the way the discussion is here (but it stated there before).

I was more thing if there is a way that we can change the imports so that everyone that imports std++ ends up in the situation that Nat.le shadows Bool.le.

stdpp.base exports Bool. Maybe it just shouldn't? Or maybe it should export NPeano (?) as well? Or else maybe stdpp.numbers should export the number/arith stuff from Coq after stdpp.base.

@robbertkrebbers No idea, it goes beyond my skills. This would probably be pertinent for Coq's standard library too. As far as I have seen there, the problem is that Bool is imported by many other files, and everything depends on the exact orders of Imports.

@jung I think it is recommended to use PeanoNat rather than NPeano. In the different patches I have done, Peano is in fact often enough.

added 4 commits

35ad2440...432120a3 - 3 commits from branch iris:master
7a0db788 - overlay for coq/coq#12162

Compare with previous version

Is there any problem with the merging of this MR? It is backward compatible.

I don't believe it is backward compatible, it seems it changes the version of le that users of std++ get.

I have prepared an alternative patch, based on @jung's suggestion above. I also avoid the deprecated NPeano and added some test cases to check that one indeed gets the right version of le. See https://gitlab.mpi-sws.org/iris/stdpp/-/commits/ci/robbert/arith

Can you test that against the Coq MR?

The possibly upcoming modifications on Coq will probably not be fully backward compatible, I agree. But with respect to the present MR, I really think it is backward compatible: it only makes a very few very little modifications on std++. Could you merge it so that discussion on the Coq side could go on? I will have a look at your patch which will be important if things move in Coq.

"Backwards compatible" here means that the more than a dozen projects that we maintain that use std++ must also keep working on both Coq 8.11 and Coq master. And given that you had to modify sets.v (and the edits arguably make the code worse), I doubt that is the case.

I understand that. Do you have evidences that it would not be the case? The modification on sets.v is replacing le by Peano.le which are the same both in Coq 8.11 and Coq master:

le : nat → nat → Prop

le is not universe polymorphic
Arguments le (_ _)%nat_scope
Expands to: Inductive Coq.Init.Peano.le

That still means we have to edit all uses of le everywhere (not sure how many there are). Something looks seriously wrong when le is not Peano.le -- that's why @robbertkrebbers proposed an alternative fix, which makes sure Peano.le remains the "default" le.

We don't want le to mean Bool.le, that just makes no sense.

@robbertkrebbers @jjourdan when grepping for le I found this in time-credits:

time-credits/theories/union_find/math/LibNatExtra.v
9:     Unfortunately [Nat.le] is NOT the same as [le], which is [Peano.le].

Seems like there's even two le on nat?!?

Concerning Nat.le, as far as I know, it is an alias for Peano.le:

Definition le := Peano.le.

in PeanoNat.v.

mentioned in commit ef839489

Concerning the MR, I think I did not make myself clear, sorry. Let me try to be better this time. There are two points:

An ongoing discussion on coq/coq#12162 which, if it is merged, will have an impact on many developments by sometimes making le mean Bool.le depending on the order of Import s. I understand this can be a major problem in many situations and it is certainly interesting to find a way to ensure this will never happen in std++ (and developments relying on it) by ensuring le to still mean Nat.le (or Peano.le) in std++ even after a potential merge of coq/coq#12162 in Coq.
The present MR which is doing very slight (backward compatible) modifications on std++ and for which I do not see potential breaking of any project (I may be wrong). I do not see any additional required modifications based on this MR only.

My question is then: would it be possible to merge the current MR (so no big impact yet)? so that the discussion on coq/coq#12162 would be meaningful (it is currently breaking Coq CI because of two projects depending on std++).

I don't see how breaking CI makes the discussion there not meaningful?

We'd like to be sure that there is a good solution that let's us use le everywhere for nat. le should not refer to Bool.le (which certainly is less frequently used, it seems like a rather esoteric operation to me). And if there is no good solution (Coq's module system is enough of a mess that this might well be the case) we'd like to work with the Coq devs to fix that. So IMO it is worthwhile to figure this out before landing a breaking change in Coq. I'd rather not land a temporary hack with some undesirable changes like explicit Peano.le, if we all agree that it is temporary (and as a permanent solution this MR here isn't great).

For that reason it would be valuable for us if you could test Robbert's branch against Coq with the patch in question.

Moreover it looks like there are plans to introduce a similar situation for lt (Bool.lt and Peano.lt). If we fix this for real now, we don't have to fix things again when that happens.

Sure, I will look at Robbert's branch.

I don't see how breaking CI makes the discussion there not meaningful?

What I mean is that, from the Coq side, the only reason the PR is not merged is CI failure. All comments there so far are supporting the merge. What would probably clarify things is if you could put comments on coq/coq#12162 explaining the troubles with std++.

Moreover it looks like there are plans to introduce a similar situation for lt (Bool.lt and Peano.lt). If we fix this for real now, we don't have to fix things again when that happens.

Agreed... I am waiting for merge of coq/coq#12008 to update coq/coq#12162. I am just trying to go on because of Coq 8.12 branching on May 15th.

If you prefer, let's stop here and move to Robbert's proposal. It would be a better long-term solution anyway. My point was just to do easy things first, trying to make the number of blocking points decrease.

@jung

use le everywhere for nat. le should not refer to Bool.le (which certainly is less frequently used, it seems like a rather esoteric operation to me)

Just a comment on this point: I perfectly agree le on Bool is not very common, but the question it raises for me is whether le should not be considered a generic enough notion so that it is not unnatural (at least in a general purpose library) that its uses have to be qualified with respect to the exact structure/type it applies on. A more specific development making a strong use of Bla.le (possibly Bla being Nat) would then introduce appropriate notations.

If Coq's module system would provide a way to make sure le is always qualified, I would be inclined to agree or at least make the experiment. But I think such an approach is hopeless to enforce with the current module system.

But also, we now already have a large body of code that uses le without qualification...

added 1 commit

90562296 - update for lt

Compare with previous version

mentioned in merge request !159 (merged)

This is updated for the current coq/coq#12162 which takes Bool.lt into account. The alternative !159 (merged) is certainly more robust.

Closing in favor of !159 (merged).

closed

overlay for coq/coq#12162

Merge request reports

Activity