adding library dependencies to compiler

Stream: lean4

[Siddharth Bhat]

In my personal fork (bollu/lean4) of the Lean4 compiler, I'd like to add a dependency to another lean library of mine that's in development: opencompl/lean-mlir. I don't know what the correct way to do such a thing is, since leanprover/lean4 does not have a leanpkg.toml to include external libraries.

• Is there some way to add a leanpkg.toml to bollu/lean4 so I can then include opencompl/lean-mlir as a dependency?
• Do I do play submodule shenanigans to include opencompl/lean-mlir within bollu/lean4?
• Some other solution I am unaware of?

[Mac]

Siddharth Bhat said:

• Do I do play submodule shenanigans to include opencompl/lean-mlir within bollu/lean4?

This is probably the best and most straightforward approach. It is also what Lean 4 does with Lake so it has been tested and show to be a viable solution.

[Siddharth Bhat]

@Mac I might well be missing something, but I was under the impression that the lean compiler itself does not use Lake modules. (I got this impression from grepping uses of lake).

In my use-case, I want to be able to use opencompl/lean-mlir/MLIR/EDSL.lean within bollu/lean4/src/Lean/Compiler/IR/EmitMLIR.lean.

I don't know how to set up paths such that EmitMLIR.lean can use the EDSL defined in opencompl/lean-mlir/../EDSL.lean
How do you suggest I set this up? I don't understand LEAN's module system very well :)

---

I suspect there will be a similar need in the hypothetical LLVM backend (leanprover/lean4/.../EmitLLVM.lean) to access (tydeu/lean4-papyrus). Will that also use a submodule?

[Henrik Böving]

I don't think how exactly other compiler backends will be integrated has been decided yet. As Leo keeps saying, the focus for now is on the mathlib port.

[Mac]

@Siddharth Bhat I guess a better question would be: is there a particular reason you need to stick your compiler backend into the Lean core itself? My plan for Papyrus was to just have the EmitLLVM.lean be in Papyrus itself rather than Lean. You can easily write an custom executable in Lean that elaborates a file itself (or import a precompiled olean) and then emits the relevant code for the module. That was my plan for Papyrus and is what I currently do in Alloy.

[Siddharth Bhat]

@Mac thank you, I'll take a look at what Alloy does.

I am quite unsure whether I want the backend to be in Lean core. It's convenient to be able to ship a backend within the compiler itself, as it simplifies things like testing. I don't know if it's a hard requirement. I have questions that will help me decide:

1. Does the strategy you have in mind for EmitLLVM.lean allow you to compile entire Lean modules/packages to LLVM? I don't know what's in an olean file. I imagine an elaborated Lean4 AST?
2. Can one test EmitLLVM.lean for correctness against the Lean4 test suite? I currently reuse the Lean4 test suite by flipping a compiler flag to emit MLIR. I don't clearly see what changes are necessary to Lean's test harness to be able to test an out of tree backend.

[Henrik Böving]

The .olean files basically give you an Environment which contains all the elaborated modules with their declarations and states of environment extensions (.e.g typeclasses are implemented as an environment extension), you can basically run any CoreM/MetaM program you want once you got an Environment.

[Mac]

Siddharth Bhat said:

Can one test EmitLLVM.lean for correctness against the Lean4 test suite?

I am not quite sure what you mean by this. Do you mean testing a Lean executable built with MLIR against the test suite? Then yes. The test suite just uses the currently available Lean executable (e.g., in PATH) to run tests. If that is the MLIR-built one, it will use that. One caveat is that you will not be able to use the CMake test driver, but will rather have to run test_single.sh directly on each test yourself.