default_extends_priority

Stream: general

[Reid Barton]

Various instances like ring_hom.monoid : monoid (α →+* α) have the wrong priority (100) because they are defined in files with set_option default_priority 100 at the top and don't specifically override the priority back to 1000.
Rather than go through and try to fix these all or add a linter to try to catch it, what if we add an option to Lean controlling the default priority used for instances generated by extends, since this seems to be the main usage of setting default_priority?

[Reid Barton]

These instances having the wrong priority is not such a big deal, but it partially defeats the purpose of lowering the instance priority of overlapping instances in the first place.
But the bigger reason for the change would be to reduce the amount of priority-related noise and especially to avoid semi-global effects like set_option default_priority--the remaining cases where a lowered priority is needed can be handled on a per-instance basis using @[priority 100] instance ....

[Reid Barton]

The purpose of adding the option wouldn't be to modify it, rather to just make the default value 100.

[Kevin Buzzard]

As a dumb check right now one can look for all occurences of default_priority in mathlib which don't have section in the line directly above -- these are the worrisome ones

[Mario Carneiro]

minor quibble: it's not really default_extends_priority but rather extends_priority because there isn't a way to set the priority directly except after the fact AFAIK

[Reid Barton]

I see what you mean

[Reid Barton]

lean#440