blob: fc05fe41b5c5f3c556717f32020d460b31c54ba9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
#!/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 1
fi
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-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
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
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}"
|
