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.
