long-running `simp`s

Stream: general

[Eric Rodriguez]

Thoughts on turning long-running simps into simp onlys even if they are terminating? I've noticed that they often crop up unrelatedly when adding simp lemmata, such as in #7692 and #7416 (note commit 3d1c124, which had to change a mostly unrelated file for simp speedups). They also lead to the exact same issues we wanted to avoid with non-terminating simps, which is having to roll back to an old version, run squeeze_simp (if it can even run without timing out! if not, even more manual fiddling) and swapping that into the new commit. Furthermore, it should speedup mathlib compilation a fair bit.

I get that they look a lot uglier, and I wonder if in the future, we could instead "cache" what simp lemmas are used in some "simp file", so that simp doesn't have to go digging for lemmas every time, which takes centuries

[Anne Baanen]

Turning simp into simp only if they take too long is an accepted practice. I believe the hope is that the switch to Lean 4's discrimination trees will speed up the situation enough that the technical solutions like a separate "simp lemma cache" are not needed yet and we accept the inconvenience of replacing the simps.

[Eric Rodriguez]

Woah, just scrolled through the Lean4 presentation; that's amazing, hopefully we can get switched to that in some not-too-far-off-point! It seems far more scalable than the current system seems to be