Timeout in geometry.manifold.vector_bundle

Stream: general

[Yaël Dillies]

docs#smooth_fibrewise_linear.locality_aux₁ has been timing out for the past few days, but it only take a second to compile and I couldn't find any significant speedup. Does someone want to give it a go?

[Jireh Loreaux]

I'm confused about this. I'm also getting timeouts on CI with this file, but when I open it locally everything is fine. Is there something wrong with the CI runners, like a bad olean cache or something?

[Floris van Doorn]

Oof, this declaration was only added recently, in #17302, and it was timing out on an earlier commit. I did some cosmetic changes, and significantly sped up some other declarations, and that seemed to have fixed it, but apparently not.
I think it has to do with the kernel type-checking the term, since I noticed the behavior that it would somehow still take quite some time to compile, after executing all tactics (unfortunately the profiler doesn't show kernel type checking time). I'll try to improve the situation.

[Floris van Doorn]

The culprit is the line choose s hs hsp φ u hu hφ h2φ heφ using h. I expect it's not worth it to fix the tactic in Lean 3, so I just expanded what choose does manually. If I give that a lot of information, the kernel checking (or whatever Lean is doing after elaboration) is noticably less. This is in PR #18507
However, I have no idea whether this actually fixes the timeout. The first commit of #18507 has the original proof twice, and somehow that doesn't time out.

[Jireh Loreaux]

I checked the original proof with various timeout settings. It seems like it's right on the border, and since deterministic timeouts aren't really deterministic (I think someone told me this), then sometimes it spills over in bors or randomly.

[Jireh Loreaux]

FYI: localality_aux₂ (on your current PR) takes rather a lot of heartbeats as well (somewhere between 85000-87500), so it will probably be okay for now. I'm just recording this here for reference unless it comes up again.

[Floris van Doorn]

Is there a better way to make choose not use this many heartbeats?

[Jireh Loreaux]

That's above my pay grade.

[Kevin Buzzard]

choose isn't hard to emulate manually with classical.some and classical.some_spec

[Jireh Loreaux]

(Aside: we don't have a "dependent choice" version of choose right? Those you have to do manually?) I should just ask this in a different thread and be more explicit about what I mean.

[Floris van Doorn]

@Kevin Buzzard that's what I did in #18507. When choosing 9 things, it's quite a bit of work.

[Yury G. Kudryashov]

How do I measure the number of heartbeats (incl. kernel typecheck)?

[Yury G. Kudryashov]

These 2 lines do the same as choose and I wnat to see if kernel typechecks faster this way:

  simp only [classical.skolem, ← exists_prop] at h,
  rcases h with ⟨s, hs, hsp, φ, u, hu, hφ, h2φ, heφ⟩,

[Yury G. Kudryashov]

At least, it compiles with -T90000.

[Yury G. Kudryashov]

@Floris van Doorn @Bryan Gin-ge Chen should we use this shorter fix?

[Yury G. Kudryashov]

I'll open a new PR on top of your PR. I don't want to bors r- your PR because I want a fix to land earlier.

[Bryan Gin-ge Chen]

Ah, nice catch!

[Yury G. Kudryashov]

#18334

[Floris van Doorn]

Thanks @Yury G. Kudryashov, your fix (#18509) is much better!