Cannot map over lists with more than 8737 elements

Stream: lean4

[Gabriel Ebner]

So I stumbled upon my first stack overflow in a year. Is there an obvious best practice workaround? Should we be using arrays instead of lists everywhere?

#eval (List.range 8738).map (. + 1) -- stack overflow
#eval toString (List.range 8737) -- stack overflow

Related question: are PRs welcome to make library functions O(1) stack size (such as the toString above), or should this be reported as issues?

[Gabriel Ebner]

(List.map could be O(1) stack as well, but I fear this would require a lot of work in the compiler.)

[Sebastian Ullrich]

All I can tell you is that Lean itself does not seem to be mapping lists of that length anywhere :) . We usually default to Array for anything of nontrivial length and when persistency/sharing is not required, yes.