Interpreter?

Stream: lean4

[Locria Cyber]

Does Lean 4 have an interpreter?

[Henrik Böving]

Since you can #eval executable lean code in your editor yes it does have an interpreter. Specifically it has an interpreter for its lowest level IR.

[Sebastian Ullrich]

http://leanprover.github.io/talks/WITS2022.pdf#page=6 (essentially true for the new compiler as well)

[Super Veridical]

Are there by any chance plans to employ LLVM jit in the future instead of the interpreter? Is the LCNF work a preparation for this or it's general intermediate representation used for optimization purposes and there are no plans for native backends other C?

[Henrik Böving]

LCNF is meant as a general IR for optimization purposes. One of the last bits of the compiler implemented in C++ right now is the optimizer and that is what the LCNF work is supposed to replace (and enhance). We are planning on writing a translator from LCNF to the current IR for garbage collection as a next step to get rid of the C++ part. At some point after that we will also replace the C backend with a LLVM one and at that point we could very much think about using the LLVM JIT for such stuff I assume? Though we haven't talked about that yet.

@Siddharth Bhat do you think that's feasible?

[Sebastian Ullrich]

I don't see sufficient motivation for adding one more compilation mode between interpretation and AOT compilation

[Mario Carneiro]

it would be great if JIT could replace the interpreter though

[Mario Carneiro]

since that would mean you don't have to support a whole separate execution environment, the same stuff that goes to AOT can go to JIT

[Sebastian Ullrich]

Issues around un- and reloading code for interactive use looked tough though, so I'm not sure if the result will be any easier. And compilation overhead is a big unknown.

[Siddharth Bhat]

@Henrik Böving conceptually, it's feasible to JIT compile the LLVM we generate. However, note that LLVM's JIT is quite slow (it spends a lot of time generating good assembly, as it was originally written for ahead-of-time compilation use-cases). Further, as @Sebastian Ullrich points out, I'm unsure how we'll manage the "state" of the JIT.