Sorry, my mistake. Apparently I mixed things up in some tests.
It is now updated with earlier and more natural insertion of `Peano`

.

**Olivier Laurent**
(964ea47b)
*
at
07 May 09:13
*

overlay for coq/coq#12162

Things are not clear to me here with respect to `Require`

/ `Import`

/ `Export`

: `Program.Syntax`

**imports** `BVector`

which **exports** `Bool`

.

done

**Olivier Laurent**
(2583846d)
*
at
07 May 08:26
*

add comment

Yes: building stdpp + !156 (closed) against coq + coq/coq#12162 gives the same errors as building std++ master against coq + coq/coq#12162.

This is updated for the current coq/coq#12162 which takes `Bool.lt`

into account.
The alternative !159 (merged) is certainly more robust.

This is an alternative to !153 which follows the spirit of !156.
It is adapted to the last version of coq/coq#12162 which takes into account the introduction of `Bool.lt`

.

**Olivier Laurent**
(90562296)
*
at
07 May 07:38
*

update for lt

For the current MR: apparently `Arith`

is not good at masking `Bool.le`

. From what I have been able to see, only `Peano`

(which contains the primary definition of `le`

) does the job.
Note also that it has to be called after any import of `Bool`

(which is in particular coming with `Program.Syntax`

through `BVector`

).
What seems to work is to add:

`From Coq Require Export Peano.`

at the end of `Require`

s in `base.v`

:

```
@@ -1,15 +1,16 @@
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, sets, and various other data
structures. *)
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Arith.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
From Coq Require Import Permutation.
Set Default Proof Using "Type".
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
+From Coq Require Export Peano.
(** This notation is necessary to prevent [length] from being printed
as [strings.length] if strings.v is imported and later base.v. See
also strings.v and
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and
```

(tested both on master and master + PR#12162)

Regarding the "spaghetti of kludges put on top of each other" of arith files in stdlib, I am also a bit lost.

Concerning `Arith`

(I did not dig into other `*Arith`

), what I understand is that `Arith`

gathers `PeanoNat`

with obsolete files. Using `PeanoNat`

and properties named `Nat.*`

is apparently the safest way to go. It apparently misses very few useful statements from my own experience. I just tried on std++: replacing `Arith`

with `PeanoNat`

works. Only one occurrence in `numbers.v`

:

```
@@ -1,9 +1,9 @@
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
-From Coq Require Export EqdepFacts PArith NArith ZArith Arith.
+From Coq Require Export EqdepFacts PArith NArith ZArith PeanoNat.
From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option.
Set Default Proof Using "Type".
Local Open Scope nat_scope.
```

I don't know for projects using std++.

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.

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 thingsagainwhen 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.

I am not 100% sure but, I think it is because of the `Module`

construction. There is this comment in `PeanoNat.v`

just above:

```
(** NB: Aliasing [le] is mandatory, since only a Definition can implement
an interface Parameter... *)
```

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++).

Concerning `Nat.le`

, as far as I know, it is an alias for `Peano.le`

:

`Definition le := Peano.le.`

in `PeanoNat.v`

.

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
```

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.

**Olivier Laurent**
(432120a3)
*
at
05 May 07:14
*

Merge branch 'ascii-countable' into 'master'

*
... and
2 more commits
*