Implement ≤-total in terms of _≤?_

[Taneb]

Fixes #2436

[gallais]

You'll need a CHANGELOG entry as it's a breaking change for people
who are relying on ≤-total's reduction behaviour on open terms.

[Taneb]

That's a good point, I'll add a changelog after #2439 gets merged

[JacquesCarette]

I'll wait to do a proper review once the CHANGELOG is in place.

[jamesmckinna]

Modulo:

• CHANGELOG
• breaking

This looks great!

[jamesmckinna]

How does this PR contribute to (positively or negatively...) the issues about 'concrete' orderings raised in issue #1179 ?
It seems as though both are trying to tackle a pervasive problem; this PR, locally, with the bigger issue at a (more) global level.

[Taneb]

@jamesmckinna they're related, but I don't think either of them solve or get in the way of the other

[jamesmckinna]

Happy to merge once there's a second 'approve' review from one of the other maintainers... and a CHANGELOG entry ;-)

[jamesmckinna]

I think when you resolve the merge conflict in CHANGELOG, you'll see that your note on this being a non-backwards compatible change has been added to the v2.1 version, and you should bring the whole of that file up-to-date with the current master/v2.2 version...?

[MatthewDaggitt]

The question is do we view this as a backwards compatible breaking change? If it was just a change in behaviour then I would say yes and bump it to v3.0. If however, we argue that this is in fact a performance bug then the maybe we can justify adding it to v2.2?

[Taneb]

@MatthewDaggitt while I would like it in sooner, of course, the position that has the better argument is that we don't make any performance guarantees at all (our readme says more or less this right near the beginning). Based on that, it probably ought wait for 3.0

[jamesmckinna]

@MatthewDaggitt while I would like it in sooner, of course, the position that has the better argument is that we don't make any performance guarantees at all (our readme says more or less this right near the beginning). Based on that, it probably ought wait for 3.0

Well, if you were to make that sacrifice, that would ease the path to a v2.2 release following #2473 ...

[Taneb]

Any objections to this being merged now?

[jamesmckinna]

Any objections to this being merged now?

Against our most recent discussion on the topic, we still do have a (placeholder?) non-breaking v2.3 milestone open, whereas breaking issues/PRs are typically being considered as v3.0? So maybe, ready though it may be, we can hold off merging for a bit? or is this mission critical to another project?

[JacquesCarette]

Do we really wish to regard relying on reduction behaviour of proofs as 'breaking'? I completely agree that, given how Agda (MLTT, really) works, lots of proofs inevitably rely on the reduction behaviour of the terms they speak about. But lifting that up a level seems a bit too far? Do we have many theorems about properties of properties?

I suspect that this change would, in fact, not affect anyone. ['suspect' indicates lower confidence that 'bet' as I'm not a big gambler.]

[jamesmckinna]

@JacquesCarette let me clarify my position:

• my understanding was that we had agreed that this was breaking, but I am happy if we row back on such a judgment
• my intention in the above was to draw attention to PRs which are clearly non-breaking/v2.3, in contrast to those which might better/best be judged v3.0...

If everyone is happy, I'd merge this for v2.3, but would advise, for belt-and-braces, that there be a "non-backwards-compatible" entry in CHANGELOG to record what's happening?

[jamesmckinna]

Or else, that we abandon the distinction v2.3/v3.0, and fast-forward to admit all the breaking changes? (We may have agreed that at the last maintainers' meeting, but for whatever reason, I'm dragging my heels...)