16721 coatoms in a t1_space

Stream: PR reviews

[Jireh Loreaux]

I'm very confused. The build failed with a deterministic timeout (this is only after having recently merged master). But when I download the oleans and run lean -T100000 src/topology/sheaves/presheaf_of_functions.lean then it happily succeeds. Also, it succeeds when I have it open in VS Code with the same 100k timeout set. So, what happened during the build? Should I just retry?

[Jireh Loreaux]

I'm going to retry, but if anyone want to take a look, here is the run: https://github.com/leanprover-community/mathlib/actions/runs/3211108316/jobs/5249043275

[Junyan Xu]

It's causing bors failure as well: https://github.com/leanprover-community/mathlib/actions/runs/3211416019/jobs/5249570763 Needs another speedup I guess!

[Jireh Loreaux]

@Junyan Xu I'm not sure it's a real problem. I just re-ran the build and it succeeded.

[Kevin Buzzard]

I am really torn by all of this. Random timeouts seem to be becoming more and more of an issue. Hopefully this will all go away with Lean 4 so perhaps the strategy is just to grit our teeth until then...

[Kevin Buzzard]

I've written the speedup. Just PRing...

[Junyan Xu]

I also PR'd #16873 ...

[Kevin Buzzard]

Thanks! You beat me to it :-) The reason I did it was that I wanted to review Chris Birkbeck's modular forms PR and he just bumped master and it timed out on the same lemma :-(

[Junyan Xu]

It turns out there are two other slow declarations in the same file that takes 13s and 4s to check respectively; the culprits again are the autofill map_id' and map_comp' fields. I've sped up them in #16873 as well. The observation is that the tactic (tidy?) used to autofill in these fields can be really slow now; presumably it wasn't the case when the file was written. Other category files have seen the same problem as well. So what has changed in the meantime? Is the slowdown due to algebraic instance hierarchy becoming more complicated (I think unlikely) or it having access to more lemmas (can we restrict the lemmas it use)?

You can see to manually fill in those fields I mostly just need ext (with cases at two locations) and refl for map_id and refl suffices for map_comp; a bit counterintuitive that id is more complicated than comp, right? This weirdness is due to the lack of definitional eta in Lean 3, so that e.g. x is not defeq to ⟨x.val, x.property⟩. With definitional eta in Lean 4, map_id should be solvable by a single refl.

[Kevin Buzzard]

Thanks! Scott once told me that things like this make him sad but at this point the speedups are more important than this I guess :-/