Compilation backend

Stream: lean4

[Shahar Papini]

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?

[Mario Carneiro]

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.

[Shahar Papini]

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?

[Mario Carneiro]

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

[Sebastian Ullrich]

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.