From 996b7b7e4a5bb259acd9f0f9a5e85f9fa2a515ca Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:06:13 +0100 Subject: [PATCH] chore(lean4): bump toolchain v4.12.0 -> v4.34.1 - lean-toolchain: leanprover/lean4:v4.34.1 - PathTraversal: List.dropLast_append_of_ne_nil no longer takes the list as an explicit argument; pass only the non-empty proof. This is the only v4.34 regression. - SymlinkOperations: trailing `/-- Summary -/` doc comment had no declaration to attach to (parse error on v4.12.0 too); make it a plain block comment. No proof changed. - rust-cli.yml lean4 job: elan --default-toolchain v4.34.1. - lakefile header: last verified v4.34.1 (2026-10-02), and list which libs build. FileContentOperations, RMOOperations, CopyMoveOperations and PermissionOperations fail on v4.12.0 as well (measured from a clean `git archive HEAD` build) and are not touched here. Theorem count 111 -> 111, sorry 0 -> 0, no axioms. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/rust-cli.yml | 2 +- proofs/lean4/PathTraversal.lean | 2 +- proofs/lean4/SymlinkOperations.lean | 2 +- proofs/lean4/lakefile.lean | 8 +++++++- proofs/lean4/lean-toolchain | 2 +- 5 files changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/rust-cli.yml b/.github/workflows/rust-cli.yml index 46863943..51e3b5f9 100644 --- a/.github/workflows/rust-cli.yml +++ b/.github/workflows/rust-cli.yml @@ -75,7 +75,7 @@ jobs: # verify its SHA-256, then execute it — no `curl | sh`. curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310 elan-init.sh" | sha256sum -c - - sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.12.0 + sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.34.1 rm -f elan-init.sh echo "$HOME/.elan/bin" >> $GITHUB_PATH diff --git a/proofs/lean4/PathTraversal.lean b/proofs/lean4/PathTraversal.lean index fcf4122f..25c90a64 100644 --- a/proofs/lean4/PathTraversal.lean +++ b/proofs/lean4/PathTraversal.lean @@ -99,7 +99,7 @@ theorem isPrefix_dropLast -- (since t :: ts is non-empty), so xs is still a prefix. refine ⟨(t :: ts).dropLast, ?_⟩ subst htail - rw [List.dropLast_append_of_ne_nil _ (List.cons_ne_nil t ts)] + rw [List.dropLast_append_of_ne_nil (List.cons_ne_nil t ts)] -- --------------------------------------------------------------------- -- Per-step invariant diff --git a/proofs/lean4/SymlinkOperations.lean b/proofs/lean4/SymlinkOperations.lean index c42fdd4f..f8635620 100644 --- a/proofs/lean4/SymlinkOperations.lean +++ b/proofs/lean4/SymlinkOperations.lean @@ -58,7 +58,7 @@ theorem symlink_unlink_reversible (p : Path) (fs : Filesystem) exact ⟨node, hfs⟩ · simp [h] -/-- Summary: +/- Summary: ✓ Symlink creation and removal operations ✓ Preconditions for safe symlink creation ✓ Reversibility: unlink(symlink(p, fs)) = fs diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean index 7aaca912..a6b9b5d7 100644 --- a/proofs/lean4/lakefile.lean +++ b/proofs/lean4/lakefile.lean @@ -1,7 +1,13 @@ -- SPDX-License-Identifier: MPL-2.0 -- Valence Shell — Lean 4 Proof Package -- --- Last verified working: Lean 4 v4.12.0 (2026-03-10) +-- Last verified working: Lean 4 v4.34.1 (2026-10-02) +-- Builds clean: FilesystemModel, FileOperations, FilesystemComposition, +-- FilesystemEquivalence, SymlinkOperations, Extraction, CrashConsistency, +-- PathTraversal, model_oracle. +-- Do NOT build (already broken on v4.12.0, not port regressions): +-- FileContentOperations, RMOOperations, CopyMoveOperations, +-- PermissionOperations. -- Toolchain pinned in: lean-toolchain -- CI workflow: .github/workflows/lean-verification.yml -- .github/workflows/rust-cli.yml (lean4 job) diff --git a/proofs/lean4/lean-toolchain b/proofs/lean4/lean-toolchain index 89985206..ba8ebf2d 100644 --- a/proofs/lean4/lean-toolchain +++ b/proofs/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.34.1