Using lean-sys crate for Rust FFI

Stream: Lean Together 2024

[Jesse Wright]

EDIT: I now have this working; and the library is published to https://github.com/jeswr/RDF.lean

I'm trying to use the lean-sys crate for FFI but hitting some blockers in doing so. Advice on how to proceed would be greatly appreciated.

• Forking the RustFFI repository and trying to use the crate results in https://github.com/jeswr/lean_sys_test (error is in readme)
• And doing so with dynamic linking results in https://github.com/jeswr/RustFFI.lean (error is in readme)

Note that my use case requires dynamic linking (see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/FFI.20with.20rust.20package.20that.20uses.20pthreads/near/418837780) so I'm primarily interested in getting the second repo working - the first repo is my attempt at creating a smaller reproduction of the issue, but I'm not sure how useful that is in this case considering it is an entirely different error that is popping up.

cc @Mario Carneiro (and thankyou for making the crate!)

[Jesse Wright]

As an update - I wanted to see how lean-sys behaved without the rest of the lean configuration noise, so tried to use it in a test in a fresh cargo package and ran into the error seen in https://github.com/jeswr/lean-sys-rust-test

[Mario Carneiro]

ah, you haven't initialized the lean runtime there

[Jesse Wright]

Ahh ty - will add that

[Jesse Wright]

https://github.com/jeswr/lean-sys-rust-test is now working - thankyou!

For the life of me I can't get this working in any setup with lean though. I am trying to get a static setup working simply adding this commit on top of this working FFI with rust. Doing so still results in the error shown here. I am stuck trying to resolve this because I don't know how to modify the flags in the leanc build step from the lakefile.lean. Any pointers to documentation describing how to do this would be greatly appreciated!

[Jesse Wright]

@Mario Carneiro I've managed to narrow down the issue in the dynamic linking case here.

EDIT It appears that one needs to disable the static feature of lean-sys; this can be done by disabling default features as follows

[dependencies]
lean-sys = { version = "0.0.5", default-features = false }

In this case the problem is that one cannot set crate-type = ["cdylib"] in a Cargo.toml where lean-sys is a dependency because lean-sys is not compiled with the -fPIC flag and thus doesn't appear to support dynamic linking use-cases. I'm not sure if there is a way of having the lean-sys package support both static and dynamic linking (I'm taking a look to see if I can figure out how to fix this now - but not particularly confident in my abilities given I'm learning rust and hence it's build system on the fly).

[Mario Carneiro]

@Jesse Wright Wait so what's the status here? Is lean-sys working both statically and dynamically now?

[Jesse Wright]

Working dynamically - and I've created a PR adding some docs to explain what confused me (https://github.com/digama0/lean-sys/pull/11). This is all I need for my use case (I am now successfully using a rust parser from Lean in https://github.com/jeswr/RustFFI.lean/pull/1 :tada:)

I haven't been able to resolve the static error case given by https://github.com/lurk-lab/RustFFI.lean/commit/a0f4ec597492aeb013c120839763a240003dfa1f

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

As far as I can tell, using lean-sys to dynamically link in libleanshared in a binary crate does not work because the binary build will not inherit the -Wl,-rpath flag (see here). (Or, rather, it does work but the RPATH is never set and you have to use LD_LIBRARY_PATH.)