leanPackages.lean4: 4.29.0 -> 4.29.1
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.
This commit is contained in:
Nadja Yang
@@ -190,6 +190,10 @@ lib.extendMkDerivation {
|
||||
mv "$out/.lake/config/[anonymous]" "$out/.lake/config/${leanPackageName}"
|
||||
fi
|
||||
|
||||
if [ -d "$out/.lake/build/ir" ]; then
|
||||
find "$out/.lake/build/ir" -name '*.setup.json' -delete
|
||||
fi
|
||||
|
||||
# Setup hook propagates LEAN_PATH to downstream packages.
|
||||
mkdir -p "$out/nix-support"
|
||||
cp ${./setup-hook.sh} "$out/nix-support/setup-hook"
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
# Test that buildLakePackage works with nix-only deps (no lake-manifest.json).
|
||||
# Test that buildLakePackage works with nix-only deps (empty lake-manifest.json).
|
||||
# Builds a Lean proof of the weak minimax inequality using mathlib.
|
||||
{
|
||||
leanPackages,
|
||||
|
||||
@@ -4,14 +4,15 @@
|
||||
fetchFromGitHub,
|
||||
}:
|
||||
|
||||
buildLakePackage {
|
||||
buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-cli";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover";
|
||||
repo = "lean4-cli";
|
||||
tag = "v4.29.0";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
|
||||
};
|
||||
|
||||
@@ -33,4 +34,4 @@ buildLakePackage {
|
||||
license = lib.licenses.mit;
|
||||
maintainers = with lib.maintainers; [ nadja-y ];
|
||||
};
|
||||
}
|
||||
})
|
||||
|
||||
@@ -6,8 +6,8 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-LeanSearchClient";
|
||||
# No lockstep tags; version pinned by mathlib's lake-manifest.json.
|
||||
version = "0-unstable-2026-02-12";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.12.0-unstable-2026-02-12";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
|
||||
@@ -6,12 +6,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-Qq";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "quote4";
|
||||
tag = "v4.29.0";
|
||||
rev = "707efb56d0696634e9e965523a1bbe9ac6ce141d";
|
||||
hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
|
||||
};
|
||||
|
||||
|
||||
@@ -7,12 +7,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-aesop";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "aesop";
|
||||
tag = "v4.29.0";
|
||||
rev = "7152850e7b216a0d409701617721b6e469d34bf6";
|
||||
hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
|
||||
};
|
||||
|
||||
|
||||
@@ -6,17 +6,28 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-batteries";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-27";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "batteries";
|
||||
tag = "v4.29.0";
|
||||
rev = "756e3321fd3b02a85ffda19fef789916223e578c";
|
||||
hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
|
||||
};
|
||||
|
||||
leanPackageName = "batteries";
|
||||
|
||||
# Pre-build static library for downstream executables.
|
||||
# TODO: upstream this to batteries
|
||||
postPatch = ''
|
||||
substituteInPlace lakefile.toml \
|
||||
--replace-fail '[[lean_lib]]
|
||||
name = "Batteries"' '[[lean_lib]]
|
||||
name = "Batteries"
|
||||
defaultFacets = ["static"]'
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "The batteries-included extended library for Lean 4";
|
||||
homepage = "https://github.com/leanprover-community/batteries";
|
||||
|
||||
@@ -7,12 +7,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-importGraph";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "import-graph";
|
||||
tag = "v4.29.0";
|
||||
rev = "48d5698bc464786347c1b0d859b18f938420f060";
|
||||
hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
|
||||
};
|
||||
|
||||
|
||||
@@ -17,7 +17,7 @@
|
||||
let
|
||||
lean4 = stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "lean4";
|
||||
version = "4.29.0";
|
||||
version = "4.29.1";
|
||||
|
||||
mimalloc-src = fetchFromGitHub {
|
||||
owner = "microsoft";
|
||||
@@ -30,7 +30,7 @@ let
|
||||
owner = "leanprover";
|
||||
repo = "lean4";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU=";
|
||||
hash = "sha256-pdhRPjSic2H8zPJXLmyfN8umKDoafjmSo4OQSRxIbyE=";
|
||||
};
|
||||
|
||||
# Vendor mimalloc. Upstream has since partially adopted FetchContent:
|
||||
|
||||
@@ -12,15 +12,16 @@
|
||||
tests,
|
||||
}:
|
||||
|
||||
buildLakePackage {
|
||||
buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-mathlib";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.1";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "mathlib4";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE=";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
|
||||
};
|
||||
|
||||
leanPackageName = "mathlib";
|
||||
@@ -44,6 +45,10 @@ buildLakePackage {
|
||||
description = "Mathematical library for Lean 4";
|
||||
homepage = "https://github.com/leanprover-community/mathlib4";
|
||||
license = lib.licenses.asl20;
|
||||
# Output exceeds Hydra's 4 GiB NAR size limit. Oleans compress well with
|
||||
# zstd (~70% ratio); a squashfs-packaged output would fit, pending upstream
|
||||
# support or a raised limit.
|
||||
hydraPlatforms = [ ];
|
||||
maintainers = with lib.maintainers; [ nadja-y ];
|
||||
};
|
||||
}
|
||||
})
|
||||
|
||||
@@ -6,12 +6,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-plausible";
|
||||
version = "4.29.0";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "plausible";
|
||||
tag = "v4.29.0";
|
||||
rev = "83e90935a17ca19ebe4b7893c7f7066e266f50d3";
|
||||
hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
|
||||
};
|
||||
|
||||
|
||||
@@ -7,23 +7,20 @@
|
||||
nodejs,
|
||||
}:
|
||||
|
||||
let
|
||||
version = "0.0.95";
|
||||
buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-proofwidgets";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "0.0.95+lean-v4.29.1";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "ProofWidgets4";
|
||||
tag = "v${version}";
|
||||
hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM=";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-D1fTsV8W29S1C53ky66sFgIoA5cLx/ilKa98czScV+s=";
|
||||
};
|
||||
in
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-proofwidgets";
|
||||
inherit version src;
|
||||
|
||||
leanPackageName = "proofwidgets";
|
||||
|
||||
# ProofWidgets has no Lean dependencies (lake-manifest.json packages = []).
|
||||
lakeHash = null;
|
||||
|
||||
nativeBuildInputs = [
|
||||
@@ -31,20 +28,14 @@ buildLakePackage {
|
||||
npmHooks.npmConfigHook
|
||||
];
|
||||
|
||||
# Pre-fetched npm dependencies for the TypeScript widget build
|
||||
# (npm/rollup in widget/). npmConfigHook installs these offline.
|
||||
npmDeps = fetchNpmDeps {
|
||||
name = "lean4-proofwidgets-npm-deps";
|
||||
inherit src;
|
||||
src = finalAttrs.src;
|
||||
sourceRoot = "source/widget";
|
||||
hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA=";
|
||||
};
|
||||
npmRoot = "widget";
|
||||
|
||||
# Lake's widgetJsAll target runs `npm clean-install` which wipes
|
||||
# node_modules and the patched shebangs that npmConfigHook applied.
|
||||
# Wrap npm to skip ci/clean-install (deps already installed) while
|
||||
# passing `npm run build` through — same pattern as llama-cpp/evcc.
|
||||
postConfigure = ''
|
||||
local realNpm
|
||||
realNpm="$(type -P npm)"
|
||||
@@ -64,4 +55,4 @@ buildLakePackage {
|
||||
license = lib.licenses.asl20;
|
||||
maintainers = with lib.maintainers; [ nadja-y ];
|
||||
};
|
||||
}
|
||||
})
|
||||
|
||||
@@ -1,30 +1,18 @@
|
||||
#!/usr/bin/env nix-shell
|
||||
#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
|
||||
#!nix-shell -i bash -p nix-update curl jq gh
|
||||
|
||||
# Update the leanPackages set.
|
||||
#
|
||||
# Usage:
|
||||
# ./pkgs/development/lean-modules/update.sh [version]
|
||||
# Usage: ./pkgs/development/lean-modules/update.sh [version]
|
||||
|
||||
set -euo pipefail
|
||||
|
||||
lean4_version="${1:-$(curl -sL https://api.github.com/repos/leanprover/lean4/releases/latest | jq -r '.tag_name' | sed 's/^v//')}"
|
||||
|
||||
# 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 "")
|
||||
dir=$(dirname "$0")
|
||||
FAKE="sha256-AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA="
|
||||
|
||||
run() { echo " $*"; "$@"; }
|
||||
old_lean4=$(nix eval --raw .#leanPackages.lean4.version 2>/dev/null || 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.
|
||||
nix-update leanPackages.lean4 --version="$lean4_version"
|
||||
|
||||
manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
|
||||
|
||||
@@ -37,47 +25,78 @@ if [ "$manifest_deps" != "$known_deps" ]; then
|
||||
exit 1
|
||||
fi
|
||||
|
||||
pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
|
||||
patch_pkg() {
|
||||
local pkgname="$1" repo="$2"
|
||||
local file="$dir/$pkgname/default.nix"
|
||||
local inputRev rev version
|
||||
inputRev=$(echo "$manifest" | jq -r ".packages[] | select(.name == \"$pkgname\") | .inputRev")
|
||||
rev=$(echo "$manifest" | jq -r ".packages[] | select(.name == \"$pkgname\") | .rev")
|
||||
|
||||
lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchClient") | .rev')
|
||||
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"
|
||||
if [[ "$inputRev" =~ ^v[0-9] ]]; then
|
||||
version="${inputRev#v}"
|
||||
# tag = "v${...version}" auto-follows; convert rev → tag if needed.
|
||||
if grep -q 'rev = "' "$file"; then
|
||||
sed -i -E "s|rev = \"[^\"]*\";|tag = \"${inputRev}\";|" "$file"
|
||||
fi
|
||||
else
|
||||
local tmp=$(mktemp -d)
|
||||
git clone --bare --filter=tree:0 --depth=100 --single-branch "https://github.com/$repo" "$tmp" 2>/dev/null
|
||||
local latest_tag=$(git -C "$tmp" describe --tags --abbrev=0 --match 'v[0-9]*' "$rev" 2>/dev/null | sed 's/^v//')
|
||||
rm -rf "$tmp"
|
||||
local date=$(gh api "repos/$repo/commits/$rev" --jq '.commit.committer.date[:10]')
|
||||
version="${latest_tag:-0}-unstable-$date"
|
||||
if grep -q 'rev = "' "$file"; then
|
||||
sed -i -E "s|rev = \"[^\"]*\";|rev = \"${rev}\";|" "$file"
|
||||
else
|
||||
sed -i -E "s|tag = \"[^\"]*\";|rev = \"${rev}\";|" "$file"
|
||||
fi
|
||||
fi
|
||||
|
||||
sed -i -E "s|version = \"[^\"]*\";|version = \"${version}\";|" "$file"
|
||||
sed -i "0,/hash = \"sha256-[^\"]*\"/{s||hash = \"$FAKE\"|}" "$file"
|
||||
}
|
||||
|
||||
echo "--- mathlib tree ---"
|
||||
|
||||
# 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
|
||||
patch_pkg batteries leanprover-community/batteries
|
||||
patch_pkg Qq leanprover-community/quote4
|
||||
patch_pkg aesop leanprover-community/aesop
|
||||
patch_pkg Cli leanprover/lean4-cli
|
||||
patch_pkg plausible leanprover-community/plausible
|
||||
patch_pkg importGraph leanprover-community/import-graph
|
||||
patch_pkg proofwidgets leanprover-community/ProofWidgets4
|
||||
patch_pkg LeanSearchClient leanprover-community/LeanSearchClient
|
||||
|
||||
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"
|
||||
|
||||
# --- summary ---
|
||||
|
||||
changes=()
|
||||
[ "$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 "status: up-to-date"
|
||||
exit 0
|
||||
sed -i -E "/lean4-mathlib/,/version/s|version = \"[^\"]*\";|version = \"${lean4_version}\";|" "$dir/mathlib/default.nix"
|
||||
if ! grep -q 'tag = "v\${finalAttrs.version}"' "$dir/mathlib/default.nix"; then
|
||||
sed -i -E 's|tag = "v[^"]*";|tag = "v${finalAttrs.version}";|' "$dir/mathlib/default.nix"
|
||||
fi
|
||||
sed -i "0,/hash = \"sha256-[^\"]*\"/{s||hash = \"$FAKE\"|}" "$dir/mathlib/default.nix"
|
||||
|
||||
echo "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version"
|
||||
echo "---"
|
||||
for c in "${changes[@]}"; do
|
||||
echo " - $c"
|
||||
prefetch() {
|
||||
local out newhash
|
||||
out=$(nix build ".#leanPackages.${1}.${2:-src}" 2>&1 || true)
|
||||
newhash=$(echo "$out" | awk '/got:/ {print $2}' | head -1)
|
||||
if [ -z "$newhash" ]; then
|
||||
echo "ERROR: failed to prefetch $1.${2:-src}" >&2
|
||||
echo "$out" >&2
|
||||
return 1
|
||||
fi
|
||||
echo "$newhash"
|
||||
}
|
||||
|
||||
for pkg in batteries Qq aesop Cli plausible importGraph proofwidgets LeanSearchClient mathlib; do
|
||||
echo " prefetching $pkg"
|
||||
newhash=$(prefetch "$pkg")
|
||||
sed -i "s|$FAKE|$newhash|" "$dir/$pkg/default.nix"
|
||||
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}"
|
||||
|
||||
echo " prefetching proofwidgets npmDeps"
|
||||
# Replace the second hash (the one inside fetchNpmDeps) with fake.
|
||||
sed -i "0,/hash = \"sha256-[^\"]*\"/!{s|hash = \"sha256-[^\"]*\"|hash = \"$FAKE\"|}" "$dir/proofwidgets/default.nix"
|
||||
newhash=$(prefetch proofwidgets npmDeps)
|
||||
sed -i "s|$FAKE|$newhash|" "$dir/proofwidgets/default.nix"
|
||||
|
||||
echo "leanPackages.lean4: $old_lean4 -> $lean4_version"
|
||||
echo "https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json"
|
||||
echo "https://github.com/leanprover/lean4/releases/tag/v${lean4_version}"
|
||||
|
||||
Reference in New Issue
Block a user