Lake+Alloy: Using external C library

Stream: lean4

[Max Nowak 🐉]

I am trying to create lean bindings for wgpu as a little weekend project (ignore that it's Wednesday please :P ).

I want to make lake download the wgpu binary release from github (or build it from source? But that requires a rust compiler). But to which directory should it be downloaded? Probably somewhere hidden inside .lake, but I have no idea how to specify that path and what the most idiomatic way is. The binary release of wgpu has both a static lib, dynamic lib, and C header files. I have tried downloading wgpu manually and adding alloy #include <?P/wgpu.h> directives myself, but I wasn't able to figure out the path ?P by trial and error.

I want to then be able to call wgpu functions from alloy functions. Since precompileModules will be on, I assume that'll require wgpu to be (dynamically) linked into every Lean module's dynlib.

[Max Nowak 🐉]

Is there documentation for lake beyond just the readme and the examples? The only relevant example is the FFI one, but it tells you how to link a library you build yourself, not an existing library. I peeked into the lake source code but it’s a lot more than I bargained for…

[Max Nowak 🐉]

Or other projects which link in external libraries.

[Kim Morrison]

Maybe need need to ping @Mac Malone here. :-)

[Mac Malone]

@Max Nowak 🐉Unfortuatenly, I do not know of any good examples of using Lake to link to external library. However, I can give some tips.

For downloading, I would suggest putting the wgpu files in a fixed top-level directory. While hiding it within .lake is possible, there is not currently good information sharing between Lake and Lean so getting the paths to its location within Lean for alloy would be difficult.

Since you mentioned the library comes with a static version, I think the simplest way to link to it is via an extern_lib lake target. For example:

extern_lib wgpu pkg :=
   inputFile <| pkg.dir / "wgpu" / "lib" / nameToStaticLib "wgpu"

To use the header files interatcively with Alloy, you can add them to the server's include path like so:

run_cmd Lean.Elab.Command.liftCoreM <|
  Alloy.C.modifyLocalServerConfig (·.addIncludePath <| "wgpu" / "include")

Similarly, you can add to Lake's include path when compiling the module like so:

lean_lib WGpu where
  weakLeancArgs := #{"-I", __dir__ / "wgpu" / "include" |>.toString]

Beware, though, I have not tested this approach myself so there could be also kinds of bugs I did not forsee. However, I would be happy to lend a hand fixing as many of them as possible time allowing.

[Utensil Song]

@Max Nowak 🐉 The lakefile.lean of LeanCopilot has been the source of inspiration of doing FFI in Lean for me. It needed to download and build C/C++ libraries (OpenBLAS and CTranslate2) from source, then link against them via FFI. If you go back in time (e.g. in this commit, after this commit onnx is removed), you'll also see how it links with a header+binary library onnxruntime.

Another inspiration would be the lakefile.lean of SciLean, it handles a header-only but C++-metaprogramming-heavy library Eigen. The pro is that it sort of established how to interface with C++ classes, particularly here. The same author also has reverse FFI work HouLean.

Personally I had worked out https://github.com/utensil/ginac-lean/blob/main/lakefile.lean that was inspired by them but it's a bit dated as I haven't worked on FFI in the last few months. Another dated little survy on this subject is here: https://github.com/utensil/ginac-lean/blob/main/doc/ffi.md . But I don't think the situation of FFI has changed significantly in the last few months, except for maybe earlier discussions 1, 2.

[Mac Malone]

@Utensil Song Your examples look great! They are also a good resource for me on what I should be stirivng to make easier in regards to FFI in Lake in the future. :)

[Max Nowak 🐉]

I have the following code so far: https://github.com/Kiiyya/lean-wgpu/tree/f77e4815cb38381924c193dadea010b3d7f0710b but have the lakefile.lean file for convenience here anyway:

import Lake
open Lake DSL

package Wgpu

require alloy from git "https://github.com/tydeu/lean4-alloy/" @ "master"

-- Need to download this yourself: https://github.com/gfx-rs/wgpu-native/releases
def wgpu_native_dir := "wgpu-macos-aarch64-debug" -- adjust this to your machine

extern_lib wgpu_native pkg :=
   inputFile <| pkg.dir / wgpu_native_dir / nameToStaticLib "wgpu_native"
  --  inputFile <| pkg.dir / wgpu_native_dir / nameToSharedLib "wgpu_native"

module_data alloy.c.o.export : BuildJob FilePath
module_data alloy.c.o.noexport : BuildJob FilePath

@[default_target]
lean_lib Wgpu where
  weakLeancArgs := #[
    "-I", __dir__ / wgpu_native_dir |>.toString
  ]
  precompileModules := true
  nativeFacets := fun shouldExport =>
    if shouldExport then #[Module.oExportFacet, `alloy.c.o.export]
    else #[Module.oNoExportFacet, `alloy.c.o.noexport]

lean_exe helloworld where
  root := `Main

The following fails:
The output of lake build helloworld --verbose is here. Oddly enough, in the LSP with #eval main, creating a WGPU instance seems to work just fine, it is only lake build helloworld that fails.

If the dynamic lib is necessary anyway, maybe deleting the static lib and doing it all with dynamic libraries would be better?

I see that even if the extern_lib declaration points to the static library file, lake generates commands with --load-dynlib=.../libwgpu_native.dylib in them. Lake was never told the name of the library, so how can it know that? (this is the output of lake build --verbose).

ℹ [36/37] Built Wgpu
trace: .> LEAN_PATH=././.lake/packages/alloy/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib:././wgpu-macos-aarch64-debug /Users/kiiya/hax/lean4/build/release/stage1/bin/lean ././././Wgpu.lean -R ./././. -o ././.lake/build/lib/Wgpu.olean -i ././.lake/build/lib/Wgpu.ilean -c ././.lake/build/ir/Wgpu.c --load-dynlib=././wgpu-macos-aarch64-debug/libwgpu_native.dylib --json
Build completed successfully.

[Max Nowak 🐉]

I will take a deeper look into the examples that Utensil Song provided, but I posted here anyway because maybe I stumbled on an easy pitfall.

[Utensil Song]

To avoid causing confusion for you, I'm bumping my lakefile.lean to the latest stable toolchain. Locally passed, waiting for CI.

(UPDATE: CI is green now, for both Ubuntu and Mac.)

[Max Nowak 🐉]

I was missing the following:

lean_exe helloworld where
  moreLinkArgs := #[
    "-framework", "Metal",
    "-framework", "QuartzCore",
    "-framework", "CoreFoundation"
  ]
  root := `Main

Finally got it to build! Awesome.

[Max Nowak 🐉]

Is it possible to only use the dynlib (or alternatively, only use the static lib)?

[Mac Malone]

Max Nowak 🐉 said:

Is it possible to only use the dynlib (or alternatively, only use the static lib)?

No, the static library is needed to statically link executables which depend on the library and the dynamic library is needed to load the library at compile time in Lean.

Support for libraries which just support dynamic linking is a future Lake todo.

[Mac Malone]

As for the lakefile, I should note that you could download the relevant wgpu library as part of the extern_lib job and stick it in some ignored directory of the package (i.e., pkg.dir / wgpu_native_dir).

[Max Nowak 🐉]

Only slightly relevant, but I don't want to open a dozen threads: Can I have some common C functions that I include in many alloy files? For example Foo.lean which contains a alloy section with C functions (i.e. not shims), which I then call from shims inside A.lean and B.lean ?

[Max Nowak 🐉]

Since alloy produces no C header files for Foo, doing import Foo inside A or B leads to the C compiler not finding the decls.

[Max Nowak 🐉]

And if I add the .lake/build/ir directory to the include path and do #include <Foo.alloy.c>, the C linker complains about duplicate symbols because now stuff is in there twice.

[Utensil Song]

Maybe you could just write these functions in plain .h/.c pairs, and let alloy include the headers just like a third party library? C in alloy only meant to be some glue code, or at most, just a .c generator, so you'll still need .h .

But if you wish alloy to generate .h alongside the .c, I guess that's also feasible.

[Max Nowak 🐉]

It looks like I asked too soon, and using of_lean<T>(..) where T is defined in a different lean module breaks as well, because the c compiler can't find the conversion function. So I'll have to do all of the glue code in one file it seems.

[Max Nowak 🐉]

So splitting the glue code up into A.lean, B.lean, ... won't help anyway.

[Max Nowak 🐉]

If I have a very simple library (the zip here) which is just one .h and one .c file, how do I tell lake to compile it and link it with my other target(s)?

[Utensil Song]

Max Nowak 🐉 said:

If I have a very simple library (the zip here) which is just one .h and one .c file, how do I tell lake to compile it and link it with my other target(s)?

You can do that by adapting target libginac_ffi and def buildCpp in my lakefile.

[Max Nowak 🐉]

I have to admit I am not having a good time with Lake. I looked at your repo, and it has a long lakefile with a lot more complexity than I had anticipated. At that point I decided to just #include <foo.c> directly instead. A new problem sprung up now, since I am on macOS and the library is actually in objective-C, I need to pass -x objective-c to the c compiler before the C file I am compiling. And moreLeancArgs get appended at the end.

[Max Nowak 🐉]

For anyone curious, this is my current (broken) lakefile.

[Mac Malone]

II fully agree that FFI i s not well supported by Lake at the moment. and doing almost anything FFI-related iis quite painful. This is a well-known issue, but I have unfortunately not had the opportunity to spend time improving it. Other things have sadly taken higher priority.

[Utensil Song]

Actually the situation is better than Mac said, it seems that I can do everything I want with the current lake FFI support, just being a little complicated which could be more convenient with future native lake support.

[Utensil Song]

I've spent last 3 days struggling with Windows FFI of my project and finally punched through. My solution is alloy-free (at the cost of complicated lakefile for now) but it should be easily adapted to alloy ones. I'll also gradually try to tidy things up in the lakefile.

I'm also on Mac so I'll investigate wgpu issues in the coming days. I'm somehow optimistic that there is a way to pass -x.

[Utensil Song]

My optimistism particularly comes from my previous experiment to make alloy emit IR in cpp and compile it.

[Utensil Song]

Particularly it's this lakefile https://github.com/utensil/lean4-alloy/blob/f09452d198a4870df147b0fbc40169358e5ab18c/lakefile.lean if you are interested to investigate yourself.

[Utensil Song]

I've modified alloy itself and made use of module_facet.

[Mac Malone]

Utensil Song said:

Actually the situation is better than Mac said, it seems that I can do everything I want with the current lake FFI support, just being a little complicated which could be more convenient with future native lake support.

Thanks for the vote of confidence! :heart: However, I do think "just being a little complicated which could be more convenient with future native lake support" is the key to the pain in question. :wink:

[Mac Malone]

Max Nowak 🐉 said:

Since alloy produces no C header files for Foo, doing import Foo inside A or B leads to the C compiler not finding the decls.

FYI, this would be a good thing to report as an issue on the alloy repo.

[Utensil Song]

@Max Nowak 🐉 I followed the instructions of your repo then run lake build, I got this:

lean-wgpu % lake -R build
✖ [104/127] Building Wgpu.Async
trace: .> LEAN_PATH=././.lake/packages/alloy/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib:././libs/wgpu-macos-aarch64-debug /Users/utensil/.elan/toolchains/leanprover--lean4---v4.8.0/bin/lean ././././Wgpu/Async.lean -R ./././. -o ././.lake/build/lib/Wgpu/Async.olean -i ././.lake/build/lib/Wgpu/Async.ilean -c ././.lake/build/ir/Wgpu/Async.c --load-dynlib=././libs/wgpu-macos-aarch64-debug/libwgpu_native.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(././libs/wgpu-macos-aarch64-debug/libwgpu_native.dylib, 0x0009): symbol not found in flat namespace '_kCAGravityTopLeft'
error: Lean exited with code 134
Some builds logged failures:
- Wgpu.Async
error: build failed

Is this expected?

[Utensil Song]

Simple googling indicates that this is caused by mixing objects that compiled with libc++ and object that compiled with libstdc++ which is a recurring theme that most third-party libraries are not compiled with libc++ but Lean seems to need it.

But can you run lake build successfully locally? I'm on Mac M1.

[Max Nowak 🐉]

The latest main branch should build just fine, I'm on an M1 mac as well. I remember _kCAGravityTopLeft not being found, and that it was fixed by specifying the right framework. Those frameworks are in the lakefile, so I'm not sure why it fails...

[Max Nowak 🐉]

The framework needed is QuartzCore.

[Max Nowak 🐉]

But I am confused why it can't find that while running lean. I thought it was about leanc (i.e. just clang).

[Utensil Song]

I see, then it might be just that my XCode didn't install the frameworks properly, will try to install them.

[Max Nowak 🐉]

XCode sometimes is weird though yeah, but specifying -framework QuartzCore should be sufficient. I think it would throw an error if it can't find the framework. And... the lakefile should specify those already when linking. Hence I'm confused.

[Utensil Song]

Then the more likely cause is that my QuartzCore is not up-to-date, so somehow it survived linking for other symbols, but failed at runtime.

[Max Nowak 🐉]

Let me know if you manage to fix it!

[Utensil Song]

I've updated XCode, accepted license, accepted the extension, and restarted Mac per instruction. Unfortunately, Lean is still trying to --load-dynlib=././libs/wgpu-macos-aarch64-debug/libwgpu_native.dylib when compiling Async.lean which has nothing to do with WGPU, then fails at the symbol issue. Will need to investigate later.

[Max Nowak 🐉]

You are on 4.8.0 right?

[Max Nowak 🐉]

I have my libs/wgpu1/libwgpu_native.dylib and libs/wgpu1/libwgpu_native.a files, which I have downloaded from github releases. In this case, lake does not overwrite anything, and merely adds a libs/wgpu1/libwgpu_native.dylib.hash file. It links against it.

...if I instead compile wgpu myself and create the same files except in the libs/wgpu2 directory, lake... overwrites (!) libs/wgpu2/libwgpu_native.dylib, which then leads to build errors. I do not know why lake doesn't overwrite it for wgpu1, but does for wgpu2.

[Max Nowak 🐉]

...yes me and a friend have been trying to get a single triangle to show for over two weeks now and still can't quite figure it out.

[Mac Malone]

@Max Nowak 🐉 Oops, this is side-effect of using inputFile for the extern_lib rather than building/downloading a static library to the package's build directory. Lake currently creates a shared library from the extern_lib static library automatically and links that. The name it uses is simply the static libraries name with a shared library extension instead of a static one. This happens to clash with the name of the shared library in the folder, hence the overwrite.

I think you got luckily with the libs/wgpu1 case in that Lake believed the shared library you had already provided to be up-to-date output of this process. This is probably because the modification time of the shared library is greater than that of the static library, whereas this was not true for the self-compiled one.

[Max Nowak 🐉]

Ah, damn. Well, I've removed the extern_lib and went back to directly linking against the dylib via -lwgpu_native, that works now.

[Yuri]

Utensil Song said:

Particularly it's this lakefile https://github.com/utensil/lean4-alloy/blob/f09452d198a4870df147b0fbc40169358e5ab18c/lakefile.lean if you are interested to investigate yourself.

@Utensil Song I tried to build your (latest) fork using lean Lean (version 4.8.0-rc1, aarch64-apple-darwin, commit dcccfb73cb24, Release) and even if I comment out all the module_facet's in the lakefile everything builds fine.

When are these module_facet's triggered?

[Utensil Song]

They are useful only for the example project https://github.com/utensil/lean4-alloy/tree/f09452d198a4870df147b0fbc40169358e5ab18c/examples/Cpp which involves generating C++ IR code. They are just a imitation of the alloy C IR code generation module facets, but with compilation setup for C++.

[Yuri]

I tried the following:

lake clean && lake build
cd examples/Cpp
lake clean && lake build

And alloy builds fine, but the Cpp project does nothing:

Cpp/.lake
├── lakefile.olean
└── lakefile.olean.trace
1 directory, 2 files

[Utensil Song]

The test programs are not set as default targets, see https://github.com/utensil/lean4-alloy/blob/master/examples/Cpp/test.sh for how to run them. They are tested on Ubuntu and Mac in CI, but last time I checked, it still has some issues on Windows.