—Categories: Formalization, Theorem Proving

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.

—Categories: Theorem Proving

Installing Isabelle 2011

I’ve spent the past few days making a few skills strides – I finally buckled down and learned how to use Emacs. The tutorial felt somewhat long but was worthwhile. Having discovered how easily I can set margins and have my text automatically wrap at 80 characters has made me a convert! Interesting since Emacs is a program I simply never thought was worth the time until I decided to try out the Isabelle theorem prover. I grabbed the 32-bit Linux bundle, ran the simple commands listed on the download page, and was up and running.

tar -xzf Isabelle2011-1_bundle_x86-linux.tar.gz
Isabelle2011-1/bin/isabelle emacs

Having completed my Emacs tutorial, I then worked through the Basic Script Management portion of the Proof General User Manual. These tasks were sufficient to prepare me for my task of analysing some proofs from The Archive of Formal Proofs.