Zulip Chat Archive

Stream: lean4

Topic: Compilation backend


view this post on Zulip Shahar Papini (Jan 26 2021 at 06:33):

Hi. I was wondering how to add a backend to the compiler, so I can compile to another architecture. Maybe it's possible to output some intermediate representation?

view this post on Zulip Mario Carneiro (Jan 26 2021 at 06:40):

At the moment, you can use lean to compile to C, which is then compiled with a standard C compiler. You can use a C compiler targeting a different architecture if you want, or you can set options in the compiler to output IR if you want. I don't know what options are available for looking at lean's own IRs.

view this post on Zulip Shahar Papini (Jan 26 2021 at 07:05):

C is too late, I need it in some functional-like IR. Can you point me to an area in the code where I can look for it?

view this post on Zulip Mario Carneiro (Jan 26 2021 at 07:09):

I know about as much about the lean 4 code as you, but https://github.com/leanprover/lean4/blob/master/src/Lean/Compiler/IR.lean looks like the main entry point to the compiler, and you can probably call those functions yourself if you want to do something else with the IR. @Leonardo de Moura will know if there is a more official way to emit IR as a compiler output

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 10:09):

There are no extension hooks for adding backends, so I would implement one as a separate Lean executable consuming .olean files via Lean.Environment.importModules. The entry point of the C backend is https://github.com/leanprover/lean4/blob/bb3a1a9699bda05e6ec44999b08438dd7a51c497/src/Lean/Compiler/IR/EmitC.lean#L726.


Last updated: May 07 2021 at 11:09 UTC