Zulip Chat Archive

Stream: lean4

I have been working on a Lean 4 interface to LLVM called Papyrus in my spare time (which I sadly will have less of now that the fall semester has started). In addition to Lean/C bindings to the LLVM C++ API, it includes a DSL for writing and manipulating LLVM IR. While this all still very much a work-in-progress, I wanted to share this little sample of what I have been able to get Lean to do:

import Papyrus

open Papyrus Script

llvm module lean_hello do
  declare %lean_object* @lean_mk_string(i8*)
  declare %lean_object* @l_IO_println___at_Lean_instEval___spec__1(%lean_object*, %lean_object*)
  define i32 @main() do
   %hello = call @lean_mk_string("Hello World!"*)
   call @l_IO_println___at_Lean_instEval___spec__1(%hello, %hello)
   ret i32 0

#dump lean_hello -- Prints the module's IR
#verify lean_hello -- Checks that the IR is valid
#jit lean_hello -- JITs the `main` function

/- #jit:
Hello World
Exited with code 0
-/

Running this code requires the library to be passed as plugin, but I think the resulting ability to write, inspect, and run IR immediately without a need for rebuilding is really cool.

Mario Carneiro (Aug 29 2021 at 01:16):

Oh, now I'm wishing for a way for the lean -> C compiler to emit code as some structured data type back into lean so that it can be retargeted to LLVM and jitted using Papyrus

Mac (Aug 29 2021 at 01:51):

@Mario Carneiro Surprisingly, the code emitter for Lean is actually quite small (it is largely one file EmitC.lean. One of future goals is to rewrite it to emit LLVM using Papyrus.

Mario Carneiro (Aug 29 2021 at 01:52):

oh, it's written in lean! I wasn't expecting that

Mario Carneiro (Aug 29 2021 at 01:52):

so yeah, you could just replace that

Mac (Aug 29 2021 at 01:52):

I still need to add support for the more of LLVM's IR before that I can do that though. The call and ret instructions are the only two currently supported. :laughing: