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.