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.