aniva
/
RustCallLean
1
0
Fork 0
Code Issues Pull Requests 1 Packages Projects Releases Wiki Activity
Example of calling Lean from Rust via the FFI
10 Commits 3 Branches 0 Tags 66 KiB
Rust 71.4%
Nix 21.5%
Lean 7.1%
Go to file
Leni Aniva 01a51b4e08
Add structure and inductive examples 		2024-03-07 21:37:37 -08:00
Callee Add structure and inductive examples 2024-03-07 21:37:37 -08:00
src Add structure and inductive examples 2024-03-07 21:37:37 -08:00
.gitignore Add bindgen hook; code cleanup 2024-03-06 13:07:54 -08:00
Cargo.lock Add bindgen hook; code cleanup 2024-03-06 13:07:54 -08:00
Cargo.toml Add bindgen hook; code cleanup 2024-03-06 13:07:54 -08:00
README.md Add usage and code cleanup 2024-03-07 00:20:02 -08:00
build.rs Code cleanup 2024-03-06 14:37:56 -08:00
flake.lock Add bindgen hook; code cleanup 2024-03-06 13:07:54 -08:00
flake.nix Code cleanup 2024-03-06 14:37:56 -08:00
rust-toolchain.toml Use stable rust. Fix `build.rs` bugs 2024-03-05 16:39:33 -08:00
rustfmt.toml Use stable rust. Fix `build.rs` bugs 2024-03-05 16:39:33 -08:00

README.md

Rust Call Lean

A tiny example of calling Lean's FFI from Rust with Nix.

This is based on:

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