This project demonstrates how to call lean code from C/C++. Main lean repository already contains an example project. Unfortunately, when your lean project depends on std or mathlib the setup gets more complicated and this repository demonstrates how to do that.
To build this repository run these commands
lake update
lake build Aesop:shared Cli:shared ImportGraph:shared Mathlib:shared ProofWidgets:shared Qq:shared Std:shared
lake build
export LIBRARY_PATH=$(pwd)/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$HOME/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/lib/lean/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/aesop/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/Cli/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/importGraph/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/mathlib/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/proofwidgets/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/Qq/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/std/.lake/build/lib/
export LD_LIBRARY_PATH=$LIBRARY_PATH
export CPLUS_INCLUDE_PATH=$HOME/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/include/
g++ test.cpp -o test -lleanshared -lreverseffiwithmathlib
./test
Let me explain what is going on:
First we download all dependencies by
lake update
Next we need to build all the dependencies and create their shared libraries
lake build Aesop:shared Cli:shared ImportGraph:shared Mathlib:shared ProofWidgets:shared Qq:shared Std:shared
This takes some time but luckily has to be done only once.
To build our project run standard lake build.
Now we have all the pieces to build test program test.cpp which uses the function minNumber defined in ReverseFFIwithMathlib.lean. The main difficulty is to tell the compiler where to find all the necessary pieces.
To tell the linker where to find all the shared libraries we set LIBRARY_PATH with
export LIBRARY_PATH=$(pwd)/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$HOME/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/lib/lean/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/aesop/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/Cli/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/importGraph/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/mathlib/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/proofwidgets/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/Qq/.lake/build/lib/
export LIBRARY_PATH=$LIBRARY_PATH:$(pwd)/.lake/packages/std/.lake/build/lib/
To find these library when we run the program we set LD_LIBRARY_PATH to the same value
export LD_LIBRARY_PATH=$LIBRARY_PATH
Specify include path when compiling c++ program using Lean C API
export CPLUS_INCLUDE_PATH=$HOME/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/include/
Compile test.cpp
g++ test.cpp -o test -lleanshared -lreverseffiwithmathlib
and run it
./test