Reverse-FFI lake example

Stream: lean4

[Riyaz Ahuja]

Hi! I made a fresh clone of the Lean4 repo so I could play with the examples src/lake/examples/reverse-ffi src/lake/examples/ffias I need a python reverse-ffi (as in, call lean functions from python) for a project i'm working on. However, I'm having trouble running test.sh in each of the examples, as they both return:

+ LAKE=../../.lake/build/bin/lake
+ ./clean.sh
+ LAKE=../../.lake/build/bin/lake
+ make run
info: downloading component 'lean'
error: could not download nonexistent lean version `lean4-stage0`
info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/lean4-stage0' to '/Users/ahuja/.elan/tmp/b62uenk3oey3gc4h_file'
info: caused by: http request returned an unsuccessful status code: 404
../../.lake/build/bin/lake --dir=lib build
make: ../../.lake/build/bin/lake: No such file or directory
make: *** [lake] Error 1

Any way to fix this so I can run the (reverse) ffi and any guidance on how to implement one for python? Thanks

[Riyaz Ahuja]

Nevermind, I figured out a good workaround and just made a simple C reverse FFI (exact same code as in the lean repo in a new project). However, how does one usually extend this to also work with functions with many dependencies to mathlib and other files in the project?

Also, is there any reasonable way to map this into python afterward (ctypes or something?)

[Derek Sorensen]

Hi all, the reverse FFI example of the lean4 repository does not compile for me. I get the error:

clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [out/main] Error 1

Any tips?

[Leni Aniva]

Derek Sorensen said:

Hi all, the reverse FFI example of the lean4 repository does not compile for me. I get the error:

clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [out/main] Error 1

Any tips?

https://leni.sh/post/240304-rust-call-lean/

I don't know if this example still works but my project is based on it. It shows a use case reverse FFI from Rust.

[Derek Sorensen]

I haven't had any luck getting your example to work @Leni Aniva :/

[Derek Sorensen]

On further inspection, when trying to use the lean-generated library, my machine complains that the __DATA_CONST segment is not read-only.

ld: __DATA_CONST segment missing SG_READ_ONLY flag in '/Users/dhsorens/devel/lean/ffi/reverse-ffi-repo/lib/.lake/build/lib/libRFFI.dylib'

[Derek Sorensen]

Is there anything that needs to be altered when building the lean library? A flag or something?

[Daniil Kisel]

Have you seen this topic? SG_READ_ONLY is mentioned here in a similar context.

[Derek Sorensen]

Nice! Thank you, this looks really relevant. No luck quite yet (after updating llvm to v19) but this gives me some more clues to work with

[Daniil Kisel]

Did you update your system's llvm? Given there is an issue on lean repo, I guess you need to update the one bundled with lean (there is one?). There is a pr with a fix which is not merged but I think you might be able to try it if you set lean-toolchain to leanprover/lean4-pr-releases:pr-release-6063.

[Derek Sorensen]

I did update my system's LLVM, and linked it to clang (as far as I know, at least). You might be right now, though I'm getting an error now: error: could not download nonexistent lean version leanprover/lean4-pr-releases:pr-release-6063`. Is there different syntax I should use for this?

[Daniil Kisel]

It seems that this PR doesn't have an associated release. I don't know what PRs get releases, maybe the problem is that it didn't pass all ci checks.

The checks on macos did pass, perhaps you could try building lean locally.

(And maybe it is possible to use some tool to modify the generated library to add the required flag? I couldn't find anything about that)

Also try setting LEAN_CC environment variable to your system's clang before building the library. It will use it for linking, maybe it will generate the correct library. (NOTE: using it like LEAN_CC=clang lake build may be wrong and an absolute path might be required, I had a problem where passing clang during some build (maybe ffi target, maybe lean target) defaulted to the lean's clang).

[Derek Sorensen]

Thanks @Daniil Kisel for all your help on this. I've put this down for now (out of exhaustion) and am just using a Linux VM to hack at the FFI for now. I'll pick this up again and come back when I have a working solution!