A work-in-progress LLVM interface for Lean 4.

Inspired by lean-llvm, which is Copyright (c) 2019 Galois, Inc. and released under the Apache 2.0 license, which can be found here: http://www.apache.org/licenses/LICENSE-2.0.

More documentation will come as development progresses. In fact, the source files are pretty well documented already (if I do say so myself), so feel free to take a look at them.

In addition to Lean/C bindings to LLVM, Papyrus also provides a DSL for writing and interacting with LLVM IR. It is still very much a work-in-progress, but here is a little sample of what it can do at the moment:

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, inttoptr (i32 1 to %lean_object*)) 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 -/

Note: To run this code, you will need to provide the PapyrusPlugin shared library (located at papyrus/plugin/build after a build) to Lean as a plugin (e.g., by providing --plugin papyrus/plugin/build/PapyrusPlugin as an argument).