Zulip Chat Archive

Stream: general

Topic: help with lean IR


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

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

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

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

view this post on Zulip Patrick Massot (Mar 25 2020 at 14:34):

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

view this post on Zulip Matthew Weingarten (Mar 25 2020 at 14:35):

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

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

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

view this post on Zulip Marc Huisinga (Mar 28 2020 at 14:06):

(deleted)

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

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

view this post on Zulip Matthew Weingarten (Mar 28 2020 at 17:22):

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

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