Commit 2023-10-11 20:05 c00742dc

View on Github →

refactor(Lean.Meta.DiscrTree): Stackless mapArrays (#7387) the naive implementation of mapArrays, when run in the interpreter, can stack overflow when creating the find_theorems cache in CI, this blocks #7244. While more fundamental fixes are possible (e.g. a Trie structure that cannot be that deep, https://github.com/leanprover/lean4/pull/2577), simply rewriting mapArrays to be a single tail-recursive function (which the interpreter is able to execute without using stack space) should prevent more unrelated PRs from failing CI.

Estimated changes