Saint's Log

Updating Lean to Avoid a Kernel Bug

I have been using Lean 4.27.0 from the beginning of the year for one of my formalization projects. I saw newer versions come along but didn’t want to have all my packages updated frequently and see all rebuilds and the associated OneDrive uploads. This is of course silly of me, but that’s how I kept going – until I saw a tweet about a lean kernel soundness bug reported in https://github.com/leanprover/lean4/issues/14576. The bug was fixed in v4.32.2. This is particularly interesting to me because it’s the first kernel bug I’ve seen since I started using lean (or really that’s been brought to my attention seeing as I might have been oblivious about previous ones, especially given my interest in avoiding any disruption updates might bring). I asked ChatGPT how to update my lean installation and walked through the steps:

saint@MacBookPro myproject % lake --version
Lake version 5.0.0-src+db93fe1 (Lean version 4.27.0)
saint@MacBookPro myproject % lean --version
Lean (version 4.27.0, arm64-apple-darwin24.6.0, commit db93fe1608548721853390a10cd40580fe7d22ae, Release)
saint@MacBookPro myproject % which lean
/Users/saint/.elan/bin/lean
saint@MacBookPro myproject % elan self update
info: downloading self-update
info: elan updated successfully to 4.2.3
saint@MacBookPro myproject % elan default leanprover/lean4:stable
info: default toolchain set to 'leanprover/lean4:stable'
saint@MacBookPro myproject % lean --version
Lean (version 4.27.0, arm64-apple-darwin24.6.0, commit db93fe1608548721853390a10cd40580fe7d22ae, Release)

The key step was updating my lean-toolchain file!

-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.32.2

Once I did this, running lean --version downloaded the latest version.

saint@MacBookPro myproject % lean --version
info: downloading https://releases.lean-lang.org/lean4/v4.32.2/lean-4.32.2-darwin_aarch64.tar.zst
524.7 MiB / 524.7 MiB (100 %)  68.3 MiB/s ETA:   0 s
info: installing /Users/saint/.elan/toolchains/leanprover--lean4---v4.32.2
Lean (version 4.32.2, arm64-apple-darwin24.6.0, commit f3b06c705e6c85f5314019d5d3baab0fec5b580c, Release)
saint@MacBookPro myproject % lean --version
Lean (version 4.32.2, arm64-apple-darwin24.6.0, commit f3b06c705e6c85f5314019d5d3baab0fec5b580c, Release)
saint@MacBookPro myproject % 

I hope to dig into the lean implementation one of these fine days and better understand how a kernel bug like this comes about.