Zulip Chat Archive

Stream: general

Topic: default_extends_priority


Reid Barton (Aug 13 2020 at 13:29):

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 (Aug 13 2020 at 13:32):

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 (Aug 13 2020 at 13:33):

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

Kevin Buzzard (Aug 13 2020 at 13:40):

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 (Aug 13 2020 at 14:15):

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 (Aug 13 2020 at 14:16):

I see what you mean

Reid Barton (Aug 13 2020 at 17:41):

lean#440


Last updated: Dec 20 2023 at 11:08 UTC