lake

Stream: lean4

[Daniel Selsam]

@Mac I am having some trouble using a lake project that includes a custom C++ target.

• Calling the C++ function in the Lean package from main works
• Calling the C++ function in the Lean package from the interpreter fails
• In a separate project, importing the first project and calling the C++ function from the interpreter also fails

I am guessing these are expected. What is the recommended setup so that e.g. a tactic can be called that wraps C++ code?

[Daniel Selsam]

Also, is it possible to create a "fake" lake project? Specifically, I would like to "wrap" the binport .oleans in such a way that it is easy to depend on them from downstream lake projects.

[Mac]

@Daniel Selsam my understanding is that in order to use C/C++ functions with interpreted Lean, you need to provide the library in question as a plugin to Lean (and, on non-Windows systems add it to LD_PRELOAD). Have you tried that? There was some useful discussion on how to do this in your mwe: plugin? thread.

[Mac]

Daniel Selsam said:

Also, is it possible to create a "fake" lake project? Specifically, I would like to "wrap" the binport .oleans in such a way that it is easy to depend on them from downstream lake projects.

This is kind of a weird use case for the current Lean package-focused Lake. When Lake eventually becomes more dynamic and can be used for arbitrary targets, this will probably be better supported.

However, you could conceivable accomplish this with the current Lake by outputting the produced .olean files in the build/lib directory of the package (so that get included in dependent packages LEAN_PATH) and even include the build process for porting .olean files in the extraDepsTarget so that it occurs ever time the package is built. However, you would still need to give Lake a dummy module root to build (though it doesn't need to actually contain anything).

[Mac]

Example added at examples/main.

[Mac]

Also, fyi, all the Lake package configuration options are now documented at the bottom of the README (and in the code itself).

[Christian Pehle]

On Linux / macOS relying on LD_PRELOAD can be avoided using a patch along the lines of https://github.com/leanprover/lean4/pull/665, that is by making the dynamic library handles part of the state of the interpreter. The way I've implemented it there is kind of a hack, but it eliminates the need for LD_PRELOAD.

[Christian Pehle]

I personally would like to see Bazel build definitions for Lean, that gives you package management and multi-language compatibility for free.

[Sebastian Ullrich]

Unfortunately Bazel does not support the kind of dynamic dependency management that is necessary to connect Lean build units according to their import statements AFAIK. Same with Meson.

[Mario Carneiro]

Aren't lean build dependencies structured just like C/C++ build dependencies? You have some #include statements and that implies a dependency order

[Sebastian Ullrich]

No, you (usually) don't compile headers before including them

[Christian Pehle]

It is true that one can't dynamically create new dependencies, but I don't see how that would be a major obstacle. BUILD files are typically written in a relatively small granularity and specifying all inputs and dependencies explicitly.

[Sebastian Ullrich]

Exactly, who'd want to do that for a Lean project?

[Christian Pehle]

If one had a lean_library rule, it wouldn't really matter if that used lean --deps internally.

[Christian Pehle]

Because all the other benefits of Bazel far outweigh the tediousness of doing that, at least for projects involving C++, external dependencies etc.

[Christian Pehle]

and lean --deps would only be used to figure out a much smaller dag (on files in the current library).

[Mac]

@Christian Pehle the goal of Lake is to create a similar build system, but with features more appropriate for Lean. The need for dynamic dependencies is just one such feature. There is also integration with the Lean server / widgets / plugins that needs to be considered.

While adapting a more mature system like Bazel certainly does have its advantages, it also means that end-users need to familiarize themselves with two languages and once again have a working dev environment. The current plan is to work towards needing no external dependencies for basic Lean use (not even a MSYS2 shell on Windows, for instance) and Bazel would be a step in the opposite direction.

It also means it would be much harder to adapt the build system as needed as Lean 4 evolves. However, I imagine an interop between Bazel and Lake/Lean would be more than welcome if someone (like you) wanted to take on the project themselves.

[Christian Pehle]

@Mac I understand that rationale. Lake seems like a great step towards making Lean usable with minimal dependencies and across platforms. Bazel is unfortunately not a lightweight dependency and other alternatives like please are niche. For the specific use case of integrating with C++/other languages it (or gn / meson) still feels preferable, since otherwise you either maintain two build systems or end up implementing the n-th C++ build system.

[Mac]

@Christian Pehle true, though Ideally the only C++ code one should be writing with Lean should be bindings. In which case, the library you are binding to should ideally already have a built dynamic/static library to link to and thus one should only be compiling the glue code, which should hopefully not be that complex to build. Though, admittedly, that is a lot of "shoulds".

[Mac]

Honestly, the more hear from you, @Christian Pehle, the more curious I am as to what you are writing that has inspired all these stated complications. I thought my LLVM bindings were are rather complex project for beta Lean 4, but whatever you are doing sounds so much more so.

[Christian Pehle]

@Mac well maybe I should be a bit more specific. For what I'm doing right now with Lean simply writing C++ binding code is sufficient. I want to use the bindings interactively (hence the plugin). I'm now experimenting with transformations in the IR and have done a simple modifications to the C backend / interpreter to support Float32 (mostly to understand how hard it would be to add additional unboxed datatypes). The next step would involve emitting to MLIR, which would probably be on the level of complexity of your really nice LLVM bindings.

At work we use one build system (waf...) for C/C++, Python, Rust, System Verilog, VHDL, manage external dependencies with Spack and deploy to Singularity containers and several embedded hardware platforms / FPGAs / simulated ASICs (a lot of our code is open source https://github.com/electronicvisions). We end up autogenerating bindings for (almost) all C++ code using libclang. In principle since Lean compiles to C it would be possible to deploy it at any level of this stack (https://github.com/GaloisInc/lean4-balance-car is a cool example).

Of course for greenfield projects and to build an open source library ecosystem a package manager like Lake is more appropriate.

[Mac]

@Christian Pehle That's really cool!

I also am especially interested in your work on adding more unboxed data types to the IR. If such a thing is feasible, it would be quite cool to do something similar in Papyrus (e.g., for arbitrary precision LLVM Integers and the various float datatypes).

[Daniel Selsam]

@Mac @Christian Pehle Thanks to both of you, I was able to get my plugin use-case working.

[Mac]

Daniel Selsam said:

Also, is it possible to create a "fake" lake project? Specifically, I would like to "wrap" the binport .oleans in such a way that it is easy to depend on them from downstream lake projects.

A side effect of the the module globs that @Mario Carneiro suggested (which are now in Lake master) is that you can now configure a package with no modules. So, a fake lake project like this should be fully possible now.