speeding up mathlib

Stream: lean4

[Kevin Buzzard]

Now #8386 has landed, mathlib compiles 20% quicker. Where is the next big speedup coming from?

One suggestion (made several times here and there on this Zulip) is that another big saving might come from decreasing the priority of instances created by extends, i.e. going back to the behaviour in lean3(c?). One suggestion made by @Sébastien Gouëzel was: 150 for parents with a direct toA field, 100 for the other ones. This would be a pretty small change in core I guess, perhaps easy for someone who knows what they're doing. Perhaps a bigger project would be to ensure that things stay that way, with a linter making sure that instances that always apply have a priority < 1000 (say 100 most of the time). Another approach, if the core devs aren't happy with this idea, would be to just make the linter and then adjust all the priorities manually.

I have seen typeclass inference going completely off the rails many times, it's trying to find a simple path involving algebra through the instance tree but all of a sudden it's thinking about topology and orders and norms and all kinds of irrelevant crazy things which aren't anywhere mentioned in the tactic state. This change would, I believe, greatly reduce the amount of crazy investigations of this form.

[Matthew Ballard]

Another non core approach would be a custom class that adds the priority adjustments automatically.

[Patrick Massot]

Is there a core Lean issue opened about this?

[Sébastien Gouëzel]

Yes, lean4#2325

[Eric Wieser]

lean4#2905 is related here too, which adds instances with priority 1000 that should not be instances at all

[Kim Morrison]

Re: lean4#2325, I think now that option 3, implemented in Mathlib, is probably the way to go here.

[Kevin Buzzard]

So this boils down to either modifying the behaviour of class in mathlib, or writing a linter?