Zulip Chat Archive

Stream: general

Topic: Tail-call elimination?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Aug 12 2018 at 17:16):

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

view this post on Zulip Sebastian Ullrich (Aug 12 2018 at 17:18):

However, 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