Topic: long-running `simp`s
Eric Rodriguez (May 28 2021 at 11:55):
Thoughts on turning long-running
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 (May 28 2021 at 11:59):
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
Eric Rodriguez (May 28 2021 at 12:12):
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
Last updated: Aug 03 2023 at 10:10 UTC