`lean4` failed to build with CMake 4.4 since CMake started putting help
strings for known variables set from the command line. Lean was using
the presence of the generic help string to determine if a variable was
passed from the command line. For CMAKE_* variables, it considers them
as platform variables if they were not passed on the command line. Those
variables are then passed only to its stage0 and not stage1. This caused
CMAKE_INSTALL_PREFIX to be dropped, since previously the nixpkgs command
line override resulted in the generic help string, and with CMake 4.4 it
no longer does.
This works around this insanity by passing STAGE1_CMAKE_INSTALL_PREFIX
which Lean understands for passing CMAKE_INSTALL_PREFIX to its stage1
build.
Lean binaries derive sysroot from IO.appPath; patch all of them
rather than just lean and lake. Add cadical to symlinkJoin paths
instead of bundling a copy via INSTALL_CADICAL.
ed10debb3c
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:
a145b9c11a
