Lean 4 in Houdini

This Houdini plugin allows you to use Lean 4 as a scripting language/replacement of VEX. This plugin is highly experimental!

Installation instructions

To build HouLean run these commands:

lake script run compileCpp /opt/hfs19.5
lake build Aesop:shared Cli:shared ImportGraph:shared LeanColls:shared Mathlib:shared ProofWidgets:shared Qq:shared SciLean:shared Std:shared
g++ -shared -o build/libLake.so -Wl,--whole-archive -fvisibility=default $HOME/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/lib/lean/libLake.a -Wl,--no-whole-archive
lake build
lake script run install ~/houdini19.5
lake script run setHoudiniEnv ~/houdini19.5  

If necessary, replace /opt/hfs19.0 with your Houdini install path and ~/houdini19.0 with Houdini preference directory.

You can find the above example scene in houdini/hip/example.hip.

TODO: explain these steps

lake build Aesop:shared Cli:shared ImportGraph:shared LeanColls:shared Mathlib:shared ProofWidgets:shared Qq:shared SciLean:shared Std:shared
g++ -shared -o build/libLake.so -Wl,--whole-archive -fvisibility=default $HOME/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/lib/lean/libLake.a -Wl,--no-whole-archive