algebra.module.linear_map mathlib4#1587

Stream: mathlib4

[Anne Baanen]

This port is almost working except for two timeouts: ext_ring_op and EndCat.ring both require about 300000 heartbeats. My usual tricks (redefining parent structures to copy over data fields, inserting intermediate definitions) don't help and in fact make the timeouts worse. How do I go about diagnosing and fixing timeouts in Lean 4?

[Kevin Buzzard]

Are you in any position to figure out whether lean4#2003 makes your life better? Is it worth trying to find speedups for this PR if that PR fixes things?

[Anne Baanen]

That's a good suggestion, thanks! Especially the ring instance seems like a candidate for being fixed.

[Anne Baanen]

You were entirely correct, lean4#2003 fixes these timeouts :octopus:

[Johan Commelin]

CI is happy with this one. But lean4#2003 isn't merged yet. Do we want to wait for that?

[Kevin Buzzard]

I asked Sebastian U about 2003 at the mathlib porting meeting yesterday and he said that there was no dev meeting this week so it's still in limbo but I guess they'll get to it when they get to it.

[Anne Baanen]

Johan Commelin said:

CI is happy with this one. But lean4#2003 isn't merged yet. Do we want to wait for that?

Right now CI passes only because I manually bump the timeout limit. So at the very least I would like to add a comment to explain why this hack is acceptable.

(There are also a few minor stylistic details that I haven't checked yet. I'll do so right now.)

[Anne Baanen]

I went through and fixed the naming convention. Since the style linter is already happy, I think the only objection to merging is the timeouts.