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.
By default, lean4's cmake copies the cadical binary from PATH to its
build output directory. Disabling this behavior does not keep Lean from
using cadical.
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:
https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2
Nadja Yang