changing algebra instance priorities

Stream: mathlib4

[Floris van Doorn]

Now that we have bumped Lean, we can finally change priorities of instances.
I believe the current instances priorities are highest for the instances that should have the lowest priority (namely, the projection to the last structure that we extend). We should experiment with making these instance priorities lowest.

[Kevin Buzzard]

Does anything good happen if you try this for some pertinent instances in the cube from CommRing to NonAssocSemiring?

[Sebastien Gouezel]

Is there a command to see the current priority of an instance?

[Eric Wieser]

Are ties on priority still broken by declaration order (latest wins)? If so, should the class command generate the instances in reverse order?

[Floris van Doorn]

Sebastien Gouezel said:

Is there a command to see the current priority of an instance?

docs#Lean.Meta.getInstancePriority?

[Floris van Doorn]

In #5941 Kevin and I changed one instance priority at the bottom of the hierarchy, and benchmarked it. Does the maxrss mean that this decreases the peak memory usage by 29%? That's pretty big!

[Johan Commelin]

Imagine what happens if we fix 10 of those instances!

[Johan Commelin]

And you seem to outline a strategy that could even be automated?

[Sebastian Ullrich]

Floris van Doorn said:

Does the maxrss mean that this decreases the peak memory usage by 29%? That's pretty big!

Yes, this appears statistically significant. We have been stuck at > 6GB for over a month while this run is at 4.4GB

[Kevin Buzzard]

branch#instance_prio2 does a few more but I'll probably have to fix the build before we can benchmark

[Eric Wieser]

Eric Wieser said:

Are ties on priority still broken by declaration order (latest wins)? If so, should the class command generate the instances in reverse order?

How hard is it to try this suggestion?

[Notification Bot]

11 messages were moved here from #mathlib4 > std4 / Lean4 bump by Eric Wieser.

[Kevin Buzzard]

I have a linter failure in #5959 which I cannot reproduce locally -- maybe some later import now makes docs#Fin.add_one_lt_iff a bad simp lemma for some reason? I am quite interested in understanding why perturbations of instance prios can cause such tiny but nonzero breakage. What is so weird and rare about these very few random lemma statements that suddenly makes them unable to unify? I'm looking at you, CovariantClass.

[Kevin Buzzard]

I am assuming that until I fix this issue, I cannot benchmark #5959 ?

[Floris van Doorn]

I opened a RFC about this at lean4#2325

[Floris van Doorn]

The TL;DR: I think we should add a linter that makes sure we use the right instances everywhere in mathlib, and maybe we can change the default extends-priorities in core.

[Kevin Buzzard]

Re the linter issue in #5959 : I can now reproduce locally, but set_option synthInstance.maxHeartbeats 40000 fixes it. Can I tell the linter to try harder or do I have to somehow fix this?

[Kevin Buzzard]

I don't know what to do here at all. The linter error is

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Data.Fin.Basic
Error: ./Mathlib/Data/Fin/Basic.lean:956:1: error: Fin.add_one_lt_iff LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CovariantClass (Fin (n + 2)) (Fin (n + 2)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

but this is the statement that b<c implies a+b<a+c for Fin (n+2), and this is not true as far as I can see.

[Eric Wieser]

I think the problem is it took too long to confirm that the statement is not true (by exhaustive search over all instances)

[Eric Wieser]

"I looked and I couldn't find the instance" is treated differently to "I tried to look but timed out before I could finish"

[Jireh Loreaux]

Kevin, just so you know, I encountered a similar problem with a simpNF call timing out, and it was in a file completely separate from the one being ported. In that case, the issue was a bad simp lemma in the new file (one which would trigger a huge amount of the time and wasn't useful), but this lemma required a Compact Space instance. So the simpNF linter was timing out looking for this instance while trying to apply this useless lemma.

[Kevin Buzzard]

I commented out simp on the erroring lemmas and I think mathlib compiled...

[Riccardo Brasca]

We have the results of !bench in #5959. It seems pretty good.

[Riccardo Brasca]

@Kevin Buzzard do you think this can help with the problem of finding instances related to subtypes? For example now

failed to synthesize
  Algebra { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 K }

happens a lot more than in mathlib3.

[Matthew Ballard]

Wall-clock is about the same?

[Kevin Buzzard]

yeah I'm not sure if these additional changes made much difference. Basically I am very interested in making algebra faster but who knows what problems this trick will solve.

[Kevin Buzzard]

I've had a bit more time to think about this. @Floris van Doorn what should happen in the following situation:

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

implies, via your rule, that Monoid.toSemigroup should be boosted and CommSemigroup.toSemigroup should have reduced priority. However

class LeftCancelMonoid (M : Type u) extends LeftCancelSemigroup M, Monoid M

implies that LeftCancelSemigroup.toSemigroup should be boosted and Monoid.toSemigroup should have reduced priority -- but we just argued that we wanted to boost it. What should I do?

[Sebastien Gouezel]

It means that we have a non-coherent library here: either both of them should first extend the monoid part and then the semigroup part, or conversely, but certainly not a mixed situation like the one you are describing.

[Matthew Ballard]

What is the rule for ordering the classes appearing after extends?

[Kevin Buzzard]

Sebastien: So you are suggesting that I redefine LeftCancelMonoid to extend these two classes but in the other order?

[Kevin Buzzard]

Matthew Ballard said:

What is the rule for ordering the classes appearing after extends?

At least one person suggested "alphabetical" :-) Can we do any better than this?

[Matthew Ballard]

Complexity?

[Kevin Buzzard]

Which is more complicated -- a monoid or a commutative semigroup? :-) Aah -- one potential tie-breaker is that one of them adds data.

[Jireh Loreaux]

I think @Eric Wieser's paper argues that there is just no coherent way to do this in general, but maybe I've misunderstood.

[Eric Wieser]

That reminds me that I should put the final version on arXiv...

[Eric Wieser]

I don't think that argument quite applies here: we're not worried about everything commuting, we just want to lay out or instance graph on a page such that the preferred parent is always the leftmost arrow (i.e. the sort order of the parents is the x position on the page)

[Jireh Loreaux]

Well, alphabetical would work I guess, until we rename something. :laughing:

[Eric Wieser]

This feels like it might be indicative that the priority mechanism is wrong. Because aren't we now attaching priorities to a class rather than an instance?

[Kevin Buzzard]

#6011 BTW

[Sebastien Gouezel]

Probably Monoid first, because it contains all the data.

[Jireh Loreaux]

But even "contains all the data" only works as long as one of the classes does that. I agree that it makes the most sense where possible though.

[Eric Wieser]

One downside of experimenting here is that every change probably causes elaboration to fail somewhere, and so trying a bunch of things introduces ugly type annotations or "obvious" implicit args, making the source marginally uglier

[Matthew Ballard]

Can we autogenerate some skeleton of the hierarchy and try to benchmark each permutation of the orderings?

[Patrick Massot]

I hope the alphabetical ordering suggestion is a joke. This order is really important. It changes what becomes a field and what gets split into pieces not overlapping the previous fields. And this has important performance implications. See the hierarchy chapter in MIL if needed.

[Matthew Ballard]

I am sure it is a joke.

[Kevin Buzzard]

class CancelMonoid (M : Type u) extends LeftCancelMonoid M, RightCancelMonoid M

Did we get this one right?

[Eric Wieser]

The alphabetical ordering was not really a joke. If we really do have to put a global order over all typeclasses, the only one that every contributor has a hope of applying instantly on the spot is sorting alphabetically

[Eric Wieser]

The fact we have to choose this global order at all seems pretty problematic to me

[Jireh Loreaux]

We can have more complicated orderings as long as we have a linter to auto-enforce it, so I don't think alphabetical is our only hope. It just needs to be sufficiently well-specified.

[Eric Wieser]

A reasonable compromise would be a text file (or DSL) that provide the arbitrary linear ordering

[Eric Wieser]

(I agree that strictly it doesn't have to be linear, but dropping that makes it harder to apply)

[Antoine Chambert-Loir]

This seems to me a good case for automatic optimization: let the computer try many choices and show which are good.

[Yury G. Kudryashov]

Unfortunately, with some choices Mathlib fails to compile (and requires little modifications here and there to fix compile), so you can't do it absolutely automatically.

[Kevin Buzzard]

Yes, see #5959 with various proof fixes caused by the priority changes.