Nadja Yang
e8db345716
Build Lean 4 projects that use the Lake build system. Dependencies can be provided as nix-packaged libraries (leanDeps) or via a fixed-output derivation that clones git deps from lake-manifest.json (lakeHash), following the same pattern as buildGoModule's vendorHash. Includes a setup hook that propagates LEAN_PATH for transitive dependency resolution.
9 lines
187 B
Bash
9 lines
187 B
Bash
addLeanPath() {
|
|
local buildLib="$1/.lake/build/lib/lean"
|
|
if [ -d "$buildLib" ]; then
|
|
addToSearchPath LEAN_PATH "$buildLib"
|
|
fi
|
|
}
|
|
|
|
addEnvHooks "$hostOffset" addLeanPath
|