help with lean IR

Stream: general

[Matthew Weingarten]

Are there some specifications for intermediate representation Lean uses? If so, where can I find them?
How can I dump the IR of a given lean program?
Thanks,
Matt

[Anton Lorenzen]

Do you mean something like the export format? https://github.com/leanprover-community/lean/blob/master/doc/export_format.md The type theory is explained in https://github.com/digama0/lean-type-theory

[Gabriel Ebner]

Another interesting IR is the bytecode used by the VM (which is used by #eval and for tactics). You can view the generated bytecode by enabling an option:

set_option trace.compiler.optimize_bytecode true
def foo (x : nat) := x + 42

[Matthew Weingarten]

Thanks for the responses Gabriel. I think the Bytecode IR is interpreted in the lean3 system is that correct? I am looking more in the direction of the lean4 IR, basically, the one described in the 'Counting Immutable Beans' as the lambda pure IR.

[Patrick Massot]

https://github.com/leanprover/lean4/

[Matthew Weingarten]

Thanks as well Anton, is this IR only used for typechecking?

[Matthew Weingarten]

Oh it took a while to click, I understand now, everything is done by set_options command in the .lean file ( so set_option trace.compiler.labda_pure true)
Thanks for the help!

[Matthew Weingarten]

Hey, what exactly is the difference between the IRs generated by these two commands?

set_option trace.compiler.ir.init true

set_option trace.compiler.lambda_pure true

Can I assume they are semantically equivalent? From anecdotal evidence on small programs they seem to produce the same code, but just show lambda-calculus functions in more 'traditional' style.

[Marc Huisinga]

(deleted)

[Simon Hudon]

The Lean 4 compiler has 2 distinct phases, one where it treats the code as pure functional code, which lambda_pure seems to print results from, and one where it uses the IR and treats it as imperative code. In functional transformations, you have things like common subexpression eliminations and constant folding and I'm not sure if lambda_pure includes those. If it does include all of those, you could see lambda_pure as the output of the functional phase and ir.init as the input of the next phase. I recommend looking through the Lean source code for lambda_pure and seeing if it has done all the functional optimizations at the time where it prints it.

[Sebastian Ullrich]

No, they are exactly the same IR. The only difference is that lambda_pure is traced from C++ and ir.init from Lean. One of them could be removed.

[Matthew Weingarten]

OK great! Thanks for the answer Sebastian, very helpful.

[Matthew Weingarten]

Also thank you Simon! I am fairly sure lambda pure includes those as it is written in the paper, that exactly the way I am looking at it so far (output of the functional phase)