Topic: help with lean IR
Matthew Weingarten (Mar 25 2020 at 11:11):
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?
Anton Lorenzen (Mar 25 2020 at 11:37):
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 (Mar 25 2020 at 11:38):
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 (Mar 25 2020 at 14:33):
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 (Mar 25 2020 at 14:34):
Matthew Weingarten (Mar 25 2020 at 14:35):
Thanks as well Anton, is this IR only used for typechecking?
Matthew Weingarten (Mar 25 2020 at 14:44):
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 (Mar 28 2020 at 14:02):
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 (Mar 28 2020 at 14:06):
Simon Hudon (Mar 28 2020 at 15:52):
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 (Mar 28 2020 at 16:03):
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 (Mar 28 2020 at 17:22):
OK great! Thanks for the answer Sebastian, very helpful.
Matthew Weingarten (Mar 28 2020 at 17:26):
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)
Last updated: May 13 2021 at 21:12 UTC