Something went wrong. Try again.
lol
Something went wrong. Try again.
3.5 kB · 83 lines
Shell
at master
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384#!/usr/bin/env nix-shell#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
# Update the leanPackages set.## 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 "")
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")
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 echo "ERROR: mathlib dependency set has changed" >&2 echo " expected: $known_deps" >&2 echo " got: $manifest_deps" >&2 exit 1fi
pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
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"
echo "--- mathlib tree ---"
# Lockstep version synchronization.dir=pkgs/development/lean-modulesfor 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
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 0fi
echo "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version"echo "---"for c in "${changes[@]}"; do echo " - $c"doneecho "---"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}"