Tail-call elimination?

Stream: general

[Keeley Hoek]

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]

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]

Lean 3's bytecode interpreter is quite basic. It does not do TCO.

[Sebastian Ullrich]

However, io.iterate needs only constant stack space: https://github.com/leanprover/lean/blob/28f4143be31b7aa3c63a907be5443ca100025ef1/src/library/vm/vm_io.cpp#L412