mlir-lean
: embedded MLIR in LEAN
This provides infrastructure for:
- An embedding of the MLIR AST in lean (
MLIR/AST.lean
) - A lightweight pretty printer library to pretty print the MLIR AST and parse errors (
MLIR/Doc.lean
) - A embedded-domain-specific language to build MLIR generic operations via macros (
MLIR/EDSL.lean
) - A parser from MLIR generic into LEAN data structures (
MLIR/MLIRParser.lean
) - A lightweight parser combinator library with error tracking (
MLIR/P.lean
)
i32
"std.return"(%zero) : (i 32) -> ()
}){sym_name = "add", type = (i32, i32) -> i32} : () -> ()
"module_terminator"() : () -> ()
}) : () -> ()
)
#print opRgnAttr0">
def opRgnAttr0 : Op := (mlir_op_call% "module"() ( { ^entry: "func"() ( { ^bb0(%arg0:i32, %arg1:i32): %zero = "std.addi"(%arg0 , %arg1) : (i32, i32) -> i32 "std.return"(%zero) : (i 32) -> () }){sym_name = "add", type = (i32, i32) -> i32} : () -> () "module_terminator"() : () -> () }) : () -> () ) #print opRgnAttr0
As a research project, we explore:
- How to provide formal semantics for MLIR, especially in the presence of multiple dialects.
- What default logics are useful, and how best to enable them for MLIR? Hoare logic? Separation logic?
- Purely functional, immutable rewriter with a carefully chosen set of primitives to enable reasoning and efficient rewriting.
Build instructions
$ lake build
$ ./build/bin/MLIR
Nix
Start a "lean shell" per the Nix Setup documentation for lean:
After installing (any version of) Nix (https://nixos.org/download.html), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
Ensure that these extra options are active in the nix you are running. Under NixOS, this means putting this in top-level config. Under a non OS level isntall, this means putting this in the .nix-profile
and restarting the nix daemon.
nix = {
package = pkgs.nixUnstable; # or versioned attributes like nix_2_4
extraOptions = ''
experimental-features = nix-command flakes
max-jobs = auto # Allow building multiple derivations in parallel
keep-outputs = true # Do not garbage-collect build time-only dependencies (e.g. clang)
# Allow fetching build results from the Lean Cachix cache
trusted-substituters = https://lean4.cachix.org/
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
allow-import-from-derivation = true
'';
};
Test instructions
$ cd examples; lit -v . # run all examples, report failures.
Documentation
- Go to
docs/README.md
for library documentation.
Other projects of interest
tydeu/lean4-papyrus
is an LLVM interface for Lean 4.GaloisInc/lean-llvm
is Lean4 bindings to the LLVM library.