| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Hydra visibility
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
|
|
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 ].
|
|
Lean 4 package set providing the mathlib dependency tree:
batteries, aesop, Qq, proofwidgets, plausible, LeanSearchClient,
Cli, importGraph, and mathlib itself.
All lockstep packages are versioned with lean4. ProofWidgets and
LeanSearchClient follow their own versioning, pinned via mathlib's
lake-manifest.json.
Includes update.sh which updates all packages to match the lean4
version in nixpkgs, with a dependency-set check to detect upstream
changes.
|
