getting started with RFFI

Stream: lean4

[Scott Kovach]

I'm trying to call Lean from C, and started with https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi linked from https://lean-lang.org/lean4/doc/dev/ffi.html
I had a few issues getting the example code to run (I'm using linux). so, first I

• call make run-local instead of make (I couldn't ultimately get the linking done by the other target to work)
• modify the makefile line 57 to remove the .lake part of the path
• install llvm15-libs

and the demo works. at that point I moved over to my project, and things also work, unless I import anything (if I've imported Foo, I get e.g. /usr/bin/ld: out/libEtch.Compile.Ext.so: undefined reference to initialize_Foo). I'm not sure how to get Lake to build everything necessary.

I tried experimenting with a single file (no imports) and ran into another issue:

@[export foo]
def foo : UInt64 := 22

@[export arr]
def arr := #[1,22,700]

@[export size]
def size (a : Array α) := a.size

the output when I try to print on the C side is

out/main-local
output: 6
size: 5229
foo: 0

suggesting these constants are not initialized. is there an extra initialization step missing from the example code?

[Scott Kovach]

or, if anyone can recommend a project using these features, I'm happy to do more investigation :thank_you:

[Utensil Song]

You may take a look at https://github.com/lecopivo/HouLean which also did RFFI.

[Utensil Song]

Particularly, here is the entry.

[Utensil Song]

If you have your code publicly on Github, I can also try reproducing the issues and investigate later.

[Sebastian Ullrich]

Also note the initialization section in the FFI doc you linked to.

you should execute code like the following exactly once before accessing any Lean declarations [...]

[Scott Kovach]

I was following the FFI doc, but the basic example still isn't working.
here's the code I'm working with: https://github.com/kovach/ffi-issue/tree/main

first commit is just the code copied from lean4 with a lean-toolchain file added (I realized the .lake issue is a new feature of v4.4.0). I've stared at the Lean manual code a few more times and I believe it matches the example there (calling lean_initialize doesn't make a difference)

second commit adds a constant UInt64 which is not initialized on the C side. try calling make run-local; for me it prints out 0 instead of 22

the Houdini code is doing something more complicated than I need, I think (using dlopen to work with dynamic libraries)