chore: Update Lean to v4.33.0 - #554

Open

argument-ci-bot[bot] wants to merge 20 commits into

mainfrom

update/lean-v4.33.0

Commits on Aug 18, 2026

chore: Update Lean to v4.33.0
samuelburnham
committed
b4d7508
ci: Use lean-update's pr setting
samuelburnham
committed
e3ff30e
chore: Adapt sources and pins to Lean v4.33.0
samuelburnham
committed
d0a3678
nix: Switch to the lean4-nix fork API
samuelburnham
committed
34ba873
chore: Move from alejandra to nixfmt
samuelburnham
committed
d6d046f
fix(tc): classify Prop up to universe normalization
samuelburnham
committed
07db29d
fix: Adapt to Lean/batteries v4.33 API changes
samuelburnham
committed
630baba
fix(ffi): decode Lean.Int by value, not as a constructor
samuelburnham
committed
9a72824
docs: Add v4.33 bump handoff
samuelburnham
committed
495d3a6
chore: Bump lean4lean to dev 4844eda and Blake3 to native-decide-dynlib
samuelburnham
committed
cee8934
fix(tc): Respell `try?` to keep its `EStateM.tryCatch` reachable
samuelburnham
committed
734009e
fix(aiur): Migrate MemSizes off deprecated Lean.RBTree
samuelburnham
committed
27d62f0
fix: Clear the two remaining v4.33 lint warnings
samuelburnham
committed
8caf2c8
test(ixvm): Repin the Slice pattern-model entry to its v4.33 name
samuelburnham
committed
162458b
chore(tc-verify): Retune the trust manifests to the new lean4lean pin
samuelburnham
committed
bfc3e6a
fix(tc-verify): Port IxTcVerify to v4.33 and the new lean4lean surface
samuelburnham
committed
1b28d7e
docs: Record v4.33 integration status and the ixvm OOM diagnosis
samuelburnham
committed
576ad93
Clippy
samuelburnham
committed
f48ecff
fmt
samuelburnham
committed
8de8e4d
Fix stale Ixon addresses
samuelburnham
committed
c377597

Navigation Menu

Uh oh!

chore: Update Lean to v4.33.0 - #554

chore: Update Lean to v4.33.0#554
argument-ci-bot[bot] wants to merge 20 commits into
mainfrom
update/lean-v4.33.0

Commits on Aug 18, 2026

chore: Update Lean to v4.33.0

ci: Use lean-update's pr setting

chore: Adapt sources and pins to Lean v4.33.0

nix: Switch to the lean4-nix fork API

chore: Move from alejandra to nixfmt

fix(tc): classify Prop up to universe normalization

fix: Adapt to Lean/batteries v4.33 API changes

fix(ffi): decode Lean.Int by value, not as a constructor

docs: Add v4.33 bump handoff

chore: Bump lean4lean to dev 4844eda and Blake3 to native-decide-dynlib

fix(tc): Respell `try?` to keep its `EStateM.tryCatch` reachable

fix(aiur): Migrate MemSizes off deprecated Lean.RBTree

fix: Clear the two remaining v4.33 lint warnings

test(ixvm): Repin the Slice pattern-model entry to its v4.33 name

chore(tc-verify): Retune the trust manifests to the new lean4lean pin

fix(tc-verify): Port IxTcVerify to v4.33 and the new lean4lean surface

docs: Record v4.33 integration status and the ixvm OOM diagnosis

Clippy

fmt

Fix stale Ixon addresses