44 lines
1.4 KiB
Markdown
44 lines
1.4 KiB
Markdown
# Rust Call Lean
|
|
|
|
A tiny example of calling Lean's FFI from Rust with Nix.
|
|
|
|
This is based on:
|
|
* [Lean4 Reverse FFI](https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi)
|
|
* [Lean4 FFI](https://lean-lang.org/lean4/doc/dev/ffi.html#initialization)
|
|
* [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html)
|
|
* [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html)
|
|
* [Rust Bindgen Static Functions](https://github.com/rust-lang/rust-bindgen/discussions/2405)
|
|
|
|
## Usage
|
|
|
|
Since the entire environment was built on Nix flakes, the easiest way to run the executable is via Nix:
|
|
```
|
|
$ nix run .#caller
|
|
```
|
|
For interactive development, one can also drop into a develop shell:
|
|
```
|
|
$ nix develop
|
|
```
|
|
and then execute
|
|
```
|
|
$ cargo run
|
|
```
|
|
Execution without Nix is possible.
|
|
|
|
This project has been tested on Linux and Mac OS.
|
|
|
|
## Structure
|
|
|
|
The project has 2 parts:
|
|
1. `Callee`, a Lean library
|
|
2. `Caller`, a Rust executable
|
|
|
|
`Caller` is dependent on `Callee` and requires it along with Lean to be present
|
|
in the environment for linking. Specifically the following environment variables
|
|
must be set:
|
|
* `CALLEE_PATH`: Path to a directory containing `libCallee.so`
|
|
* `LEAN_ROOT`: Path to a directory such that `$LEAN_ROOT/include` has lean
|
|
headers and `$LEAN_ROOT/lib` has the `leanshared` library
|
|
* Clang path must be set so `clang-sys` can find it
|
|
* Clang executable must be present in `PATH`
|