Strip ephemeral setup.json build artifacts from library outputs.
These are produced per-module during compilation and not included
in upstream cache distributions
(https://github.com/NixOS/nixpkgs/issues/510957).
Disable Hydra builds for mathlib since the output exceeds the NAR
size limit.
Pre-build static library for batteries so downstream executables
can link against it.
Refactor update.sh to pin each dependency to the rev from mathlib's
lake-manifest.json.
Give leanPackages its own lean4, independent of pkgs.lean4. Binary-
patch the toolchain so the language server discovers the wrapped lake
despite lake serve deriving LAKE from IO.appPath unconditionally.
Supplant Lake's config trace validation for /nix/store/ dependencies,
deferring cache coherence to Nix.
Migrate Nix-managed dependency injection from package-overrides.json
to lake --packages. Patch Cli to pre-build static library for
downstream executables. Add recurseIntoAttrs for Hydra.
Upstream accepted FetchContent for mimalloc vendoring:
a145b9c11a
Verifies that buildLakePackage works with nix-only deps (no
lake-manifest.json). Builds a proof of the weak minimax inequality
from Mathlib.Order.CompleteLattice.Basic using leanDeps = [ mathlib ].
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.
