mathport drops priorities in `attribute [instance]`

Stream: mathlib4

[Scott Morrison]

mathport drops priorities when we add instance after the fact. e.g. attribute [instance, priority 100] just turning into attribute [instance], when it should probably be attribute [instance 100]. There are many many cases of this. Should we fix mathport? Re-port these priorities?

[Scott Morrison]

These missing priorities just recently resulted in @Joël Riou running into a mysterious timeout at https://github.com/leanprover-community/mathlib4/pull/3595.

[Joël Riou]

The other timeouts in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20class.20inference.20problem may be related to this. However, the fix found by @Scott Morrison does not seem to work there.

[Mario Carneiro]

Fixed in mathport

[Scott Morrison]

I ported the things we previously missed at https://github.com/leanprover-community/mathlib4/pull/3613

[Scott Morrison]

This doesn't include any local attributes, or priorities on coercion related instances.

[Eric Wieser]

A lot of those priorities still don't seem to show up in the mathport output

[Mario Carneiro]

any examples in particular?

[Mario Carneiro]

that diff seems to be full of fixes

[Mario Carneiro]

but I can't see the fixes that didn't happen

[Mario Carneiro]

specifically, what was the syntactic context of a priority annotation that was skipped

[Mario Carneiro]

I wouldn't be too surprised if one was missed, because the lean 3 way of writing priorities is somewhat indirect

[Eric Wieser]

!4#3613 is full of attributes in CategoryTheory that aren't present in the mathport output

[Mario Carneiro]

what was the lean 3 code?

[Mario Carneiro]

you are asking me to diff 4 things here

[Eric Wieser]

I don't know whether that's because Scott added new ones or because mathport just forgot them

[Eric Wieser]

These lines

[Eric Wieser]

Sorry, I think I'm just struggling to match up Scott's diff to mathport'

[Eric Wieser]

Those are in mathport after all

[Mario Carneiro]

I think all of scott's changes are in the diff

[Floris van Doorn]

Many instance priorities in the algebraic hierarchy are also "wrong" (different from mathlib3) since we cannot change the priorities of classes extending other classes (cf. lean4#2115)