Topic: Tail-call elimination?
Keeley Hoek (Aug 12 2018 at 11:08):
Because I have no idea how the VM actually works I tempt asking a meaningless question here, but here we go regardless: does the VM do tail-call elimination? Will my IO reading loops eventually explode if left to their own devices for long enough?
Simon Hudon (Aug 12 2018 at 17:13):
I don't remember seeing that mentioned anywhere but that's a pretty basic optimization and Leo is pretty aggressive on optimization so I don't doubt he saw to it right away.
Sebastian Ullrich (Aug 12 2018 at 17:16):
Lean 3's bytecode interpreter is quite basic. It does not do TCO.
Sebastian Ullrich (Aug 12 2018 at 17:18):
io.iterate needs only constant stack space: https://github.com/leanprover/lean/blob/28f4143be31b7aa3c63a907be5443ca100025ef1/src/library/vm/vm_io.cpp#L412
Last updated: May 06 2021 at 22:13 UTC