bug in `ext`?

Stream: mathlib4

[Yury G. Kudryashov]

I started porting fiber bundle trivializations in !4#2707, and the first @[ext] fails.

[Yury G. Kudryashov]

For the case if I push a workaround before this issue is resolved, the relevant commit is 92feef9.

[Oliver Nash]

If we do find a bug in ext then I think it would be worth seeing how it affects the situation here. I had intended to debug the ext issue there a bit more but the PR got merged before I got a chance.

I also learned from @Jireh Loreaux that in Lean 4, @[ext] lemmas may carry user-defined priorities whereas in Lean 3 the tactic apparently discriminated between which qualifying lemma to apply according to order of definition.

[Jireh Loreaux]

Oliver, I think the "priority" in mathlib 3 was just whichever lemma was declared latest.

[Jireh Loreaux]

So, IIUC it didn't "discriminate" as you suggest.

[Jireh Loreaux]

I think the data structure holding ext lemmas in Lean 4 now has no history in the sense of which declaration was declared most recently, so it needs a manual priority.

[Oliver Nash]

Agreed! I have attempted to communicate what you say here. My use of the word "discriminate" was not intended to imply the tactic kept more state that it did.

[Oliver Nash]

Or to put it another way: one may implement "most recently defined" discrimination using constant space.

[Eric Wieser]

Jireh Loreaux said:

Oliver, I think the "priority" in mathlib 3 was just whichever lemma was declared latest.

More precisely, in lean 3 lemmas are sorted lexicographically by (priority, global declaration index)

[Eric Wieser]

So declaration order breaks ties in priority

[Eric Wieser]

Which turned out to always be the correct choice for ext, to the point that I think we never set priorities manually.

[Yury G. Kudryashov]

The bug I'm talking about is in the ext attribute, not in the ext tactic.

[Yury G. Kudryashov]

It fails to generate ext lemmas.

[Gabriel Ebner]

https://github.com/leanprover/std4/pull/106

[Jeremy Tan]

@Gabriel Ebner see my request for access to mathlib4 so I can port files

[Scott Morrison]

Jeremy Tan said:

Gabriel Ebner see my request for access to mathlib4 so I can port files

@Jeremy Tan, no need to crosspost on random threads, please. :-)