From 3c2a3b804d85fde7c4c00a2cdc2da85bd75743e5 Mon Sep 17 00:00:00 2001 From: Nadja Yang Date: Sat, 28 Mar 2026 13:53:22 -0400 Subject: [PATCH] =?UTF-8?q?leanPackages:=20structural=20reimagining=20?= =?UTF-8?q?=E2=80=94=20own=20toolchain,=20lake=20--packages,=20Hydra=20vis?= =?UTF-8?q?ibility?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- pkgs/build-support/lake/default.nix | 178 +++++------------- .../lake/test/weak-minimax/Main.lean | 4 - .../lake/test/weak-minimax/lake-manifest.json | 1 + .../lake/test/weak-minimax/lakefile.lean | 4 - .../lake/test/weak-minimax/package.nix | 26 +-- pkgs/development/lean-modules/Cli/default.nix | 16 +- .../lean-modules/LeanSearchClient/default.nix | 6 - pkgs/development/lean-modules/Qq/default.nix | 6 +- .../lean-modules/aesop/default.nix | 6 +- .../lean-modules/batteries/default.nix | 6 +- .../lean-modules/importGraph/default.nix | 6 +- .../lean-modules/lean4/default.nix | 138 ++++++++++++++ .../lean-modules/mathlib/default.nix | 8 +- .../lean-modules/plausible/default.nix | 6 +- .../lean-modules/proofwidgets/default.nix | 11 +- pkgs/development/lean-modules/update.sh | 90 ++++----- pkgs/top-level/all-packages.nix | 2 +- pkgs/top-level/lean-packages.nix | 27 +-- 18 files changed, 274 insertions(+), 267 deletions(-) delete mode 100644 pkgs/build-support/lake/test/weak-minimax/Main.lean create mode 100644 pkgs/build-support/lake/test/weak-minimax/lake-manifest.json create mode 100644 pkgs/development/lean-modules/lean4/default.nix diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix index 42344a7797ff..114a8354fa89 100644 --- a/pkgs/build-support/lake/default.nix +++ b/pkgs/build-support/lake/default.nix @@ -1,20 +1,11 @@ # buildLakePackage: build Lean 4 projects that use the Lake build system. # # Dependencies can be provided in two ways: -# - `leanDeps`: already-packaged Lean libraries from leanPackages. -# These are injected into LEAN_PATH via setup hooks and propagated -# transitively, similar to Haskell's libraryHaskellDepends. +# - `leanDeps`: nix-packaged Lean libraries, injected via +# `lake --packages` and propagated transitively via LEAN_PATH. # - `lakeHash`: SRI hash for a fetchLakeDeps FOD that clones git # dependencies listed in lake-manifest.json (like buildGoModule's # vendorHash). Not needed when all deps are in `leanDeps`. -# -# Library output layout: -# $out/ Package root (source + build artifacts) -# $out/lakefile.{lean,toml} Lake package configuration -# $out/lean-toolchain Lean version pin -# $out/.lake/build/lib/lean/ Compiled .olean/.ilean files -# $out/.lake/build/ir/ Compiled C/object files -# $out/nix-support/setup-hook LEAN_PATH propagation hook { lib, stdenv, @@ -22,7 +13,7 @@ gitMinimal, cacert, jq, - lndir, + writeText, stdenvNoCC, }: @@ -55,32 +46,19 @@ lib.extendMkDerivation { nativeBuildInputs ? [ ], passthru ? { }, - # SRI hash for the Lake dependencies FOD. - # Set to null if the project has no external dependencies - # (or all deps are provided via leanDeps). + # SRI hash for the Lake dependencies FOD (null = all deps nix-managed). lakeHash ? null, - # Pre-built Lake dependencies derivation (overrides lakeHash). lakeDeps ? null, - - # Already-packaged Lean libraries from nixpkgs. - # These are added to LEAN_PATH (via setup hook) and propagated - # transitively. Each must be a buildLakePackage output with - # .olean files under $out/.lake/build/lib/lean/. + # Nix-packaged Lean libraries, injected via lake --packages. leanDeps ? [ ], - - # Lean package name as declared in lakefile.lean/toml. - # Defaults to pname. + # Lake package name as declared in lakefile (defaults to pname). leanPackageName ? finalAttrs.pname, - - # Lake build targets. Empty list means the default target. + # Lake build targets (empty = default targets). buildTargets ? [ ], - - # Whether this is a library (install full package tree with - # .olean/.ilean files) or an executable (install binaries only). + # Library (install .olean tree) or executable (install binaries only). isLibrary ? true, - - # Override attributes of the lakeDeps derivation. + # Override the FOD derivation attrs. overrideLakeDepsAttrs ? (finalAttrs: previousAttrs: { }), meta ? { }, @@ -96,6 +74,10 @@ lib.extendMkDerivation { isLibrary = args.isLibrary or true; leanPackageName = args.leanPackageName or finalAttrs.pname; + allLeanDeps = lib.unique ( + builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps + ); + computedLakeDeps = if lakeDeps' != null then lakeDeps' @@ -114,11 +96,18 @@ lib.extendMkDerivation { }).overrideAttrs (lib.toExtension overrideLakeDepsAttrs); - # Transitively collect all Lean dependencies. Each buildLakePackage - # library stores its own transitive closure in passthru.allLeanDeps, - # so this flattens the entire dependency DAG. - allLeanDeps = lib.unique ( - builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps + # Nix-managed dep overrides, generated at eval time. + # --packages takes precedence over .lake/package-overrides.json. + overridesFile = writeText "lake-overrides.json" ( + builtins.toJSON { + schemaVersion = "1.2.0"; + packages = map (dep: { + type = "path"; + name = dep.passthru.lakePackageName or dep.pname; + inherited = false; + dir = "${dep}"; + }) allLeanDeps; + } ); in { @@ -128,14 +117,9 @@ lib.extendMkDerivation { lean4 gitMinimal jq - lndir ]; - # Propagate so downstream packages get transitive LEAN_PATH entries - # via each dependency's nix-support/setup-hook. propagatedBuildInputs = lib.optionals isLibrary leanDeps; - - # Executables only need deps at build time. buildInputs = lib.optionals (!isLibrary) leanDeps; configurePhase = @@ -144,106 +128,34 @@ lib.extendMkDerivation { export HOME="$TMPDIR" - # Disable Lake cloud caching and Reservoir lookups + # Disable cloud caching and Reservoir lookups. export LAKE_NO_CACHE=1 export RESERVOIR_API_URL="" - - # Point leanc at the nix-provided C compiler export LEAN_CC="${stdenv.cc}/bin/cc" - # Validate that the lean-toolchain file (if present) matches the - # Lean toolchain we are building against. Mismatches between the - # toolchain version and the compiler produce confusing errors, so - # fail early with a clear message. - leanVersion="${lean4.version}" - if [ -f lean-toolchain ]; then - toolchainVersion=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' lean-toolchain) - if [ -n "$toolchainVersion" ] && [ "$toolchainVersion" != "$leanVersion" ]; then - echo "buildLakePackage: lean-toolchain requests v$toolchainVersion but lean4 is v$leanVersion" >&2 - echo "buildLakePackage: update the package or use a matching lean4 version" >&2 - exit 1 - fi - fi - - ${lib.concatStringsSep "\n" ( - builtins.map ( - dep: - let - name = dep.passthru.lakePackageName or dep.pname; - in - '' - # Fail fast if nix-packaged dep "${name}" was built against a - # different Lean version. This avoids wasting build time when - # the package set is mid-update (e.g. lean4 bumped but a dep - # has not been updated yet). - if [ -f "${dep}/lean-toolchain" ]; then - depToolchain=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' "${dep}/lean-toolchain") - if [ -n "$depToolchain" ] && [ "$depToolchain" != "$leanVersion" ]; then - echo "buildLakePackage: dependency ${name} was built with Lean v$depToolchain but lean4 is v$leanVersion" >&2 - echo "buildLakePackage: update ${name} first, or override lean4 in leanPackages" >&2 - exit 1 - fi - fi - '' - ) allLeanDeps - )} - if [ -n "''${LEAN_PATH:-}" ]; then echo "buildLakePackage: LEAN_PATH=$LEAN_PATH" fi - mkdir -p .lake/packages - - # Create a minimal empty manifest if none exists. Lake requires - # this file, but when all deps come from leanDeps (nix-managed), - # the actual dependency entries come from package-overrides.json. - if [ ! -f lake-manifest.json ]; then - echo '{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}' \ - > lake-manifest.json - fi - ${lib.optionalString (computedLakeDeps != null) '' - # Copy fetched (not yet nix-packaged) deps into .lake/packages/ + mkdir -p .lake/packages for dep in ${computedLakeDeps}/*; do depName="$(basename "$dep")" cp -r "$dep" ".lake/packages/$depName" chmod -R u+w ".lake/packages/$depName" done - ''} - ${lib.concatStringsSep "\n" ( - builtins.map ( - dep: - let - name = dep.passthru.lakePackageName or dep.pname; - in - '' - # Install nix-packaged dep "${name}" into .lake/packages/. - # lndir creates a symlink tree so artifacts remain as - # zero-copy references to the store; writable dirs let Lake - # create metadata during workspace initialization. - rm -rf ".lake/packages/${name}" - mkdir -p ".lake/packages/${name}" - lndir -silent "${dep}" ".lake/packages/${name}" - '' - ) allLeanDeps - )} - - # Generate package-overrides.json redirecting deps to local - # paths. Scans .lake/packages/ so that nix-managed deps work - # even without a lake-manifest.json (like Haskell's package DB - # approach — nix is the sole dependency provider, Lake just - # validates against lakefile.lean at build time). - if [ -d .lake/packages ] && [ -n "$(ls -A .lake/packages/ 2>/dev/null)" ]; then + # FOD deps use package-overrides.json (the on-disk mechanism). + # Nix-managed deps use --packages (the CLI mechanism, takes precedence). jq -n --argjson pkgs "$( for dep in .lake/packages/*/; do [ -d "$dep" ] || continue depName="$(basename "$dep")" - printf '{"type":"path","name":"%s","inherited":false,"configFile":"lakefile","dir":".lake/packages/%s"}\n' \ - "$depName" "$depName" + jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \ + '{type: "path", name: $name, inherited: false, dir: $dir}' done | jq -s '.' - )" '{schemaVersion: "1.1.0", packages: $pkgs}' > .lake/package-overrides.json - fi + )" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json + ''} runHook postConfigure ''; @@ -255,7 +167,7 @@ lib.extendMkDerivation { local targets="${lib.concatStringsSep " " buildTargets}" echo "buildLakePackage: building ''${targets:-default targets}" - lake build --no-ansi $targets + lake build --no-ansi --packages=${overridesFile} $targets runHook postBuild ''; @@ -266,25 +178,22 @@ lib.extendMkDerivation { '' runHook preInstall - # Install the complete Lake package tree. $out/ IS the - # package directory — source, lakefile, and pre-built - # artifacts under .lake/build/. + # Install the complete Lake package tree. cp -rT . "$out" - # Remove build-environment artifacts that reference the - # build sandbox or dependency store paths. + # Remove build-time artifacts. rm -rf "$out/.lake/packages" rm -f "$out/.lake/package-overrides.json" - # Install the setup hook so that downstream derivations - # (and `nix develop` shells) automatically get this - # package's oleans in LEAN_PATH. + # Reconcile config trace directory naming. + if [ -d "$out/.lake/config/[anonymous]" ]; then + mv "$out/.lake/config/[anonymous]" "$out/.lake/config/${leanPackageName}" + fi + + # Setup hook propagates LEAN_PATH to downstream packages. mkdir -p "$out/nix-support" cp ${./setup-hook.sh} "$out/nix-support/setup-hook" - # Symlink any built executables into $out/bin/ for - # discoverability (e.g. packages that are both libraries - # and executables). if [ -d "$out/.lake/build/bin" ]; then mkdir -p "$out/bin" for exe in "$out/.lake/build/bin"/*; do @@ -300,7 +209,6 @@ lib.extendMkDerivation { '' runHook preInstall - # Install executables only. if [ -d .lake/build/bin ]; then mkdir -p "$out/bin" find .lake/build/bin -type f -executable \ @@ -314,8 +222,6 @@ lib.extendMkDerivation { passthru = passthru // { inherit computedLakeDeps lean4 allLeanDeps; lakePackageName = leanPackageName; - # Canonicalize overrideLakeDepsAttrs as an attribute overlay, - # following the same pattern as buildGoModule's overrideModAttrs. overrideLakeDepsAttrs = lib.toExtension overrideLakeDepsAttrs; }; diff --git a/pkgs/build-support/lake/test/weak-minimax/Main.lean b/pkgs/build-support/lake/test/weak-minimax/Main.lean deleted file mode 100644 index 490b95b07e82..000000000000 --- a/pkgs/build-support/lake/test/weak-minimax/Main.lean +++ /dev/null @@ -1,4 +0,0 @@ -import WeakMinimax - -def main : IO Unit := do - IO.println "weak_minimax: verified (maximin <= minimax)" diff --git a/pkgs/build-support/lake/test/weak-minimax/lake-manifest.json b/pkgs/build-support/lake/test/weak-minimax/lake-manifest.json new file mode 100644 index 000000000000..ef86e4de986a --- /dev/null +++ b/pkgs/build-support/lake/test/weak-minimax/lake-manifest.json @@ -0,0 +1 @@ +{"version":"1.1.0","packagesDir":".lake/packages","packages":[]} diff --git a/pkgs/build-support/lake/test/weak-minimax/lakefile.lean b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean index 9937799396d1..670adcbf345c 100644 --- a/pkgs/build-support/lake/test/weak-minimax/lakefile.lean +++ b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean @@ -6,7 +6,3 @@ package weakMinimax require "leanprover-community" / "mathlib" @ git "main" @[default_target] lean_lib WeakMinimax - -@[default_target] -lean_exe weakMinimax.run where - root := `Main diff --git a/pkgs/build-support/lake/test/weak-minimax/package.nix b/pkgs/build-support/lake/test/weak-minimax/package.nix index 5e6114486792..19cecab89878 100644 --- a/pkgs/build-support/lake/test/weak-minimax/package.nix +++ b/pkgs/build-support/lake/test/weak-minimax/package.nix @@ -1,12 +1,5 @@ # Test that buildLakePackage works with nix-only deps (no lake-manifest.json). # Builds a Lean proof of the weak minimax inequality using mathlib. -# -# Note: building the executable recompiles .c → .c.o for all transitive -# dependency modules because library packages only ship .olean/.ilean/.c -# artifacts (the default Lake library facet). Lake's trace system would -# reuse pre-built object files if present, but since Lean 4 is rarely -# used for application code, we defer shipping .o files in library -# packages to keep store footprint minimal. { leanPackages, runCommand, @@ -24,17 +17,10 @@ let }; in -runCommand "buildLakePackage-weak-minimax" - { - nativeBuildInputs = [ testPackage ]; - } - '' - mkdir -p $out +runCommand "buildLakePackage-weak-minimax" { } '' + mkdir -p $out - # Verify the executable runs (proof was verified at build time). - weakMinimax-run | tee $out/result - grep -q "weak_minimax" $out/result - - # Verify library output has compiled oleans. - test -d "${testPackage}/.lake/build/lib/lean" - '' + # Verify library output has compiled oleans. + test -d "${testPackage}/.lake/build/lib/lean" + touch $out/success +'' diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix index 0177c09973db..d3bc495ee9cf 100644 --- a/pkgs/development/lean-modules/Cli/default.nix +++ b/pkgs/development/lean-modules/Cli/default.nix @@ -6,17 +6,27 @@ buildLakePackage { pname = "lean4-cli"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover"; repo = "lean4-cli"; - tag = "v4.28.0"; - hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4="; + tag = "v4.29.0"; + hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk="; }; leanPackageName = "Cli"; + # Pre-build static library for downstream executables. + # TODO: upstream this to lean4-cli + postPatch = '' + substituteInPlace lakefile.toml \ + --replace-fail '[[lean_lib]] + name = "Cli"' '[[lean_lib]] + name = "Cli" + defaultFacets = ["static"]' + ''; + meta = { description = "Command-line argument parser for Lean 4"; homepage = "https://github.com/leanprover/lean4-cli"; diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix index bce5fe166814..b7e25b5ecbd0 100644 --- a/pkgs/development/lean-modules/LeanSearchClient/default.nix +++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix @@ -18,12 +18,6 @@ buildLakePackage { leanPackageName = "LeanSearchClient"; - # Upstream lean-toolchain lags behind; remove it so the - # buildLakePackage toolchain check does not reject this package. - postPatch = '' - rm -f lean-toolchain - ''; - meta = { description = "Lean 4 client for LeanSearch and Moogle proof search"; homepage = "https://github.com/leanprover-community/LeanSearchClient"; diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix index 6939b121939c..6feb6fa51916 100644 --- a/pkgs/development/lean-modules/Qq/default.nix +++ b/pkgs/development/lean-modules/Qq/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-Qq"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "quote4"; - tag = "v4.28.0"; - hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ="; + tag = "v4.29.0"; + hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0="; }; leanPackageName = "Qq"; diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix index e60651dbe2a0..7d8ad308741a 100644 --- a/pkgs/development/lean-modules/aesop/default.nix +++ b/pkgs/development/lean-modules/aesop/default.nix @@ -7,13 +7,13 @@ buildLakePackage { pname = "lean4-aesop"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "aesop"; - tag = "v4.28.0"; - hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4="; + tag = "v4.29.0"; + hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg="; }; leanPackageName = "aesop"; diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix index af0b8623e1c6..9fdb1efd8686 100644 --- a/pkgs/development/lean-modules/batteries/default.nix +++ b/pkgs/development/lean-modules/batteries/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-batteries"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "batteries"; - tag = "v4.28.0"; - hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc="; + tag = "v4.29.0"; + hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ="; }; leanPackageName = "batteries"; diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix index 50a91b3c819f..4da481fd5a16 100644 --- a/pkgs/development/lean-modules/importGraph/default.nix +++ b/pkgs/development/lean-modules/importGraph/default.nix @@ -7,13 +7,13 @@ buildLakePackage { pname = "lean4-importGraph"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "import-graph"; - tag = "v4.28.0"; - hash = "sha256-fZS8bFQjV7eLZCJwD+SVRzmCcCthrl+PO8vL8U8AOYs="; + tag = "v4.29.0"; + hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg="; }; leanPackageName = "importGraph"; diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix new file mode 100644 index 000000000000..e53d298db06f --- /dev/null +++ b/pkgs/development/lean-modules/lean4/default.nix @@ -0,0 +1,138 @@ +# Lean 4 toolchain for the leanPackages set (independent of pkgs.lean4). +{ + lib, + stdenv, + symlinkJoin, + cmake, + fetchFromGitHub, + git, + gmp, + cadical, + pkg-config, + libuv, + perl, + testers, +}: + +let + lean4 = stdenv.mkDerivation (finalAttrs: { + pname = "lean4"; + version = "4.29.0"; + + mimalloc-src = fetchFromGitHub { + owner = "microsoft"; + repo = "mimalloc"; + tag = "v2.2.3"; + hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74="; + }; + + src = fetchFromGitHub { + owner = "leanprover"; + repo = "lean4"; + tag = "v${finalAttrs.version}"; + hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU="; + }; + + # Vendor mimalloc. Upstream has since partially adopted FetchContent: + # https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2 + # + # Dynamically adjust the source tree to maintain a healthy boundary + # with Nix and avoid overstepping on its jurisdiction over cache coherence. + postPatch = + let + pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc"; + in + '' + substituteInPlace src/CMakeLists.txt \ + --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")' + + rm -rf src/lake/examples/git/ + + substituteInPlace CMakeLists.txt \ + --replace-fail 'GIT_REPOSITORY https://github.com/microsoft/mimalloc' \ + 'SOURCE_DIR "${finalAttrs.mimalloc-src}"' \ + --replace-fail 'GIT_TAG ${finalAttrs.mimalloc-src.tag}' "" + for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do + substituteInPlace "$file" \ + --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}' + done + + substituteInPlace src/lake/Lake/Load/Lean/Elab.lean \ + --replace-fail \ + 'let upToDate := (← olean.pathExists) ∧' \ + 'let upToDate := cfg.pkgDir.toString.startsWith "/nix/store/" ∨ (← olean.pathExists) ∧' + ''; + + preConfigure = '' + patchShebangs stage0/src/bin/ src/bin/ + ''; + + nativeBuildInputs = [ + cmake + pkg-config + ]; + + buildInputs = [ + gmp + libuv + cadical + ]; + + nativeCheckInputs = [ + git + perl + ]; + + cmakeFlags = [ + "-DUSE_GITHASH=OFF" + "-DINSTALL_LICENSE=OFF" + "-DUSE_MIMALLOC=ON" + ]; + + passthru.tests = { + version = testers.testVersion { + package = finalAttrs.finalPackage; + version = "v${finalAttrs.version}"; + }; + }; + + meta = { + description = "Automatic and interactive theorem prover"; + homepage = "https://leanprover.github.io/"; + changelog = "https://github.com/leanprover/lean4/blob/${finalAttrs.src.tag}/RELEASES.md"; + license = lib.licenses.asl20; + platforms = lib.platforms.all; + maintainers = with lib.maintainers; [ nadja-y ]; + mainProgram = "lean"; + }; + }); + + oldStorePath = builtins.substring 0 43 (toString lean4); +in +# Binary-patched for correct runtime discovery in wrapped environments. +symlinkJoin { + inherit (lean4) name pname; + paths = [ lean4 ]; + nativeBuildInputs = [ perl ]; + postBuild = '' + newStorePath=$(echo "$out" | head -c 43) + + # Copy (not symlink) — IO.appPath resolves through symlinks. + rm $out/bin/lean $out/bin/lake + cp ${lean4}/bin/lean $out/bin/lean + cp ${lean4}/bin/lake $out/bin/lake + + for bin in $out/bin/lean $out/bin/lake; do + cat "$bin" \ + | perl -pe "s|\Q${oldStorePath}\E|$newStorePath|g" \ + > "$bin.tmp" + chmod +x "$bin.tmp" + mv "$bin.tmp" "$bin" + done + ''; + + inherit (lean4) version src meta; + passthru = { + inherit (lean4) version src; + }; +} diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix index 77d935a79a44..70a34dd9f333 100644 --- a/pkgs/development/lean-modules/mathlib/default.nix +++ b/pkgs/development/lean-modules/mathlib/default.nix @@ -14,13 +14,13 @@ buildLakePackage { pname = "lean4-mathlib"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "mathlib4"; - tag = "v4.28.0"; - hash = "sha256-7kR0WvEDey5kEdqKKVEO/JgQd1VyB6a+zwPvIV5E5Pg="; + tag = "v4.29.0"; + hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE="; }; leanPackageName = "mathlib"; @@ -34,6 +34,8 @@ buildLakePackage { importGraph ]; + requiredSystemFeatures = [ "big-parallel" ]; + passthru.tests = { inherit (tests.lake) weak-minimax; }; diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix index dc61bca2c751..07b22b3ebe87 100644 --- a/pkgs/development/lean-modules/plausible/default.nix +++ b/pkgs/development/lean-modules/plausible/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-plausible"; - version = "4.28.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "plausible"; - tag = "v4.28.0"; - hash = "sha256-xuOfeoRPt5L0Rk4fEJPIi1A0aoNIkC1fsh5yeIx5bFI="; + tag = "v4.29.0"; + hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50="; }; leanPackageName = "plausible"; diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix index c026f0c62bcc..54998125b500 100644 --- a/pkgs/development/lean-modules/proofwidgets/default.nix +++ b/pkgs/development/lean-modules/proofwidgets/default.nix @@ -8,19 +8,18 @@ }: let + version = "0.0.95"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "ProofWidgets4"; - tag = "v0.0.87"; - hash = "sha256-qXEqNfwUBPnxAtLRkBZTBFhrM4JYl43gLo/PM6HOG7o="; + tag = "v${version}"; + hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM="; }; in buildLakePackage { pname = "lean4-proofwidgets"; - version = "0.0.87"; - - inherit src; + inherit version src; leanPackageName = "proofwidgets"; @@ -38,7 +37,7 @@ buildLakePackage { name = "lean4-proofwidgets-npm-deps"; inherit src; sourceRoot = "source/widget"; - hash = "sha256-CzBRrreOSytquZ/xFHPlY8r+lz5Bg9Zk9ienRhc8SiY="; + hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA="; }; npmRoot = "widget"; diff --git a/pkgs/development/lean-modules/update.sh b/pkgs/development/lean-modules/update.sh index a02e52d6775f..fc05fe41b5c5 100755 --- a/pkgs/development/lean-modules/update.sh +++ b/pkgs/development/lean-modules/update.sh @@ -1,33 +1,33 @@ #!/usr/bin/env nix-shell #!nix-shell -i bash -p nix-update common-updater-scripts curl jq -# Update all leanPackages to match the lean4 version in nixpkgs. -# -# All mathlib-ecosystem packages (batteries, aesop, Qq, plausible, -# importGraph, Cli, mathlib) release with the same version tag as -# lean4 (lockstep versioning). ProofWidgets and LeanSearchClient -# have their own versioning; the correct versions are read from -# mathlib's lake-manifest.json at the matching lean4 tag. -# -# This script only prefetches source hashes — it does not build -# anything. Output is a summary suitable for commit messages. +# Update the leanPackages set. # # Usage: -# ./pkgs/development/lean-modules/update.sh +# ./pkgs/development/lean-modules/update.sh [version] set -euo pipefail -lean4_version=$(nix eval --raw .#lean4.version) +lean4_version="${1:-$(curl -sL https://api.github.com/repos/leanprover/lean4/releases/latest | jq -r '.tag_name' | sed 's/^v//')}" -# Snapshot current versions for diffing. +# Snapshot before any updates. old_lockstep=$(nix eval --raw .#leanPackages.mathlib.version 2>/dev/null || echo "") old_pw=$(nix eval --raw .#leanPackages.proofwidgets.version 2>/dev/null || echo "") old_lsc=$(nix eval --raw .#leanPackages.LeanSearchClient.version 2>/dev/null || echo "") +run() { echo " $*"; "$@"; } + +# --- lean4 toolchain --- + +run nix-update leanPackages.lean4 --version="$lean4_version" + +# --- mathlib dependency tree --- +# Versions are derived from mathlib's lake-manifest.json at the +# matching lean4 tag. Most packages release in lockstep with lean4; +# ProofWidgets and LeanSearchClient have their own versioning. + manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json") -# Verify that mathlib's dependency set matches what we package. -# If mathlib adds or removes a dep, this script needs manual updating. known_deps="Cli LeanSearchClient Qq aesop batteries importGraph plausible proofwidgets" manifest_deps=$(echo "$manifest" | jq -r '[.packages[].name] | sort | join(" ")') if [ "$manifest_deps" != "$known_deps" ]; then @@ -43,41 +43,41 @@ lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchCli lsc_date=$(curl -sL "https://api.github.com/repos/leanprover-community/LeanSearchClient/commits/$lsc_rev" | jq -r '.commit.committer.date[:10]') lsc_version="0-unstable-$lsc_date" -# Leaf packages (no leanDeps). -nix-update leanPackages.batteries --version="$lean4_version" -nix-update leanPackages.Qq --version="$lean4_version" -nix-update leanPackages.plausible --version="$lean4_version" -nix-update leanPackages.Cli --version="$lean4_version" -nix-update leanPackages.proofwidgets --version="$pw_version" +echo "--- mathlib tree ---" -# LeanSearchClient has no lockstep tags; pin to the exact rev mathlib uses. -update-source-version leanPackages.LeanSearchClient "$lsc_version" \ - --rev="$lsc_rev" +# Lockstep version synchronization. +dir=pkgs/development/lean-modules +for pkg in batteries aesop Qq plausible Cli importGraph mathlib; do + sed -i "s|tag = \"v${old_lockstep}\"|tag = \"v${lean4_version}\"|" "$dir/$pkg/default.nix" +done -# Packages with leanDeps. -nix-update leanPackages.aesop --version="$lean4_version" -nix-update leanPackages.importGraph --version="$lean4_version" +run nix-update leanPackages.batteries --version="$lean4_version" +run nix-update leanPackages.Qq --version="$lean4_version" +run nix-update leanPackages.plausible --version="$lean4_version" +run nix-update leanPackages.Cli --version="$lean4_version" +run nix-update leanPackages.proofwidgets --version="$pw_version" +run update-source-version leanPackages.LeanSearchClient "$lsc_version" --rev="$lsc_rev" +run nix-update leanPackages.aesop --version="$lean4_version" +run nix-update leanPackages.importGraph --version="$lean4_version" +run nix-update leanPackages.mathlib --version="$lean4_version" -# mathlib (all deps are nix-packaged, no lakeHash needed). -nix-update leanPackages.mathlib --version="$lean4_version" +# --- summary --- -# Summary. changes=() -if [ "$old_lockstep" != "$lean4_version" ]; then - changes+=("lockstep packages: $old_lockstep -> $lean4_version") -fi -if [ "$old_pw" != "$pw_version" ]; then - changes+=("proofwidgets: $old_pw -> $pw_version") -fi -if [ "$old_lsc" != "$lsc_version" ]; then - changes+=("LeanSearchClient: $old_lsc -> $lsc_version") -fi +[ "$old_lockstep" != "$lean4_version" ] && changes+=("mathlib tree: $old_lockstep -> $lean4_version") +[ "$old_pw" != "$pw_version" ] && changes+=("proofwidgets: $old_pw -> $pw_version") +[ "$old_lsc" != "$lsc_version" ] && changes+=("LeanSearchClient: $old_lsc -> $lsc_version") if [ ${#changes[@]} -eq 0 ]; then - echo "leanPackages: already up to date at lean4 $lean4_version" -else - echo "leanPackages: update to lean4 $lean4_version" - for c in "${changes[@]}"; do - echo " - $c" - done + echo "status: up-to-date" + exit 0 fi + +echo "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version" +echo "---" +for c in "${changes[@]}"; do + echo " - $c" +done +echo "---" +echo "manifest-source: https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json" +echo "lean4-release: https://github.com/leanprover/lean4/releases/tag/v${lean4_version}" diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ff68d58a5eb7..8b8752d4a59c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -2853,7 +2853,7 @@ with pkgs; leanblueprint = with python3Packages; toPythonApplication leanblueprint; - leanPackages = callPackage ../top-level/lean-packages.nix { }; + leanPackages = recurseIntoAttrs (callPackage ../top-level/lean-packages.nix { }); inherit (callPackage ../development/tools/lerna { }) lerna_6 diff --git a/pkgs/top-level/lean-packages.nix b/pkgs/top-level/lean-packages.nix index 64314343a910..7bdc715217cb 100644 --- a/pkgs/top-level/lean-packages.nix +++ b/pkgs/top-level/lean-packages.nix @@ -1,45 +1,24 @@ -# Lean 4 package set. +# Lean 4 package set with its own toolchain (independent of pkgs.lean4). # -# All packages are built against a single Lean toolchain version. -# Dependencies between packages use `leanDeps` which propagates -# .olean files via LEAN_PATH (through setup hooks), similar to how -# Haskell propagates package.conf.d entries. -# -# Overriding lean4 propagates to all packages in the set: +# Override the toolchain for the entire set: # leanPackages.overrideScope (self: super: { lean4 = lean4-custom; }) -# -# Usage: -# leanPackages.batteries -# leanPackages.mathlib -# leanPackages.callPackage ./my-package.nix { } { lib, newScope, - lean4, }: lib.makeScope newScope (self: { - inherit lean4; + lean4 = self.callPackage ../development/lean-modules/lean4 { }; - # Resolve via self.callPackage so overriding lean4 in the scope - # propagates to the builder (same pattern as coqPackages). buildLakePackage = self.callPackage ../build-support/lake { }; batteries = self.callPackage ../development/lean-modules/batteries { }; - aesop = self.callPackage ../development/lean-modules/aesop { }; - Qq = self.callPackage ../development/lean-modules/Qq { }; - proofwidgets = self.callPackage ../development/lean-modules/proofwidgets { }; - plausible = self.callPackage ../development/lean-modules/plausible { }; - LeanSearchClient = self.callPackage ../development/lean-modules/LeanSearchClient { }; - Cli = self.callPackage ../development/lean-modules/Cli { }; - importGraph = self.callPackage ../development/lean-modules/importGraph { }; - mathlib = self.callPackage ../development/lean-modules/mathlib { }; })