From ed306d1177d562800898d90757745236feac1ed4 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 18 Oct 2026 20:05:30 -0300 Subject: [PATCH] chore(deps): bump Lean toolchain and dependencies to v4.35.0 Pin cslib, verso, doc-gen4 and Mathlib to their v4.35.0 tags. Follow Mathlib's renames of Mathlib.Data.Rel and Mathlib.Data.Setoid.Basic, update the expected #print Rel output (Rel now ranges over Sort), and replace the deprecated String.mk with String.ofList. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author. --- CSwL/InfEngine.lean | 2 +- CSwL/Sets.lean | 6 ++--- CSwLCompat.lean | 3 +-- CSwLMeta/Save/Project.lean | 4 ++-- README.md | 2 +- lake-manifest.json | 46 +++++++++++++++++++------------------- lakefile.toml | 21 +++++++++-------- lean-toolchain | 2 +- 8 files changed, 42 insertions(+), 44 deletions(-) diff --git a/CSwL/InfEngine.lean b/CSwL/InfEngine.lean index 178e02f..66c6d13 100644 --- a/CSwL/InfEngine.lean +++ b/CSwL/InfEngine.lean @@ -336,7 +336,7 @@ pontuação, e quebrando em palavras. def preprocess (line : String) : List String := let kept := line.toList.takeWhile (fun c => c.isAlpha || c.isWhitespace) - (String.mk kept).toLower.splitOn " " + (String.ofList kept).toLower.splitOn " " |>.filter (fun w => w ≠ "") ``` diff --git a/CSwL/Sets.lean b/CSwL/Sets.lean index 2832fe8..99fb2e9 100644 --- a/CSwL/Sets.lean +++ b/CSwL/Sets.lean @@ -1,13 +1,13 @@ import CSwLMeta import Bib import Mathlib.Algebra.Group.Nat.Even -import Mathlib.Data.Rel +import Mathlib.Basic.Rel import Mathlib.Logic.Relation import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Insert import Mathlib.Data.Finset.Prod import Mathlib.Data.Fintype.Prod -import Mathlib.Data.Setoid.Basic +import Mathlib.Order.Setoid.Basic import Mathlib.Tactic open Verso.Genre Manual @@ -443,7 +443,7 @@ nenhuma — é a definição: ``` ```leanOutput c3print3 -@[reducible] def Rel.{u_6, u_7} : Type u_6 → Type u_7 → Type (max u_6 u_7) := +@[reducible] def Rel.{u_6, u_7} : Sort u_6 → Sort u_7 → Sort (max (max 1 u_6) u_7) := fun α β => α → β → Prop ``` diff --git a/CSwLCompat.lean b/CSwLCompat.lean index d59e365..888b1f9 100644 --- a/CSwLCompat.lean +++ b/CSwLCompat.lean @@ -16,8 +16,7 @@ -- 2. No `namespace Tests` from the end of the original -- `SFLCompat/Experiment.lean`: those are `#guard_msgs` that check the -- exact text of Lean diagnostics ("Unknown identifier `x`", literal --- positions via `(positions := true)`, etc.). `CSwL` is on the same --- `v4.33.0` as `sf-in-lean` today, but pinning that text here risks +-- positions via `(positions := true)`, etc.). Pinning that text here risks -- breaking both the book's build and every extracted project's build -- (the file is copied verbatim) on any message drift between Lean -- versions -- with no payoff for the course, which uses neither `recall` diff --git a/CSwLMeta/Save/Project.lean b/CSwLMeta/Save/Project.lean index 7e92a43..a4347d6 100644 --- a/CSwLMeta/Save/Project.lean +++ b/CSwLMeta/Save/Project.lean @@ -88,7 +88,7 @@ structure ExtractConfig where build` is about three seconds. It is not rebuilt on every `make`, but `make clean` removes `_out/` and the next build pays for it again. The toolchain objection that once kept this off is gone -- the generated - project and `CSwL` are both on `v4.33.0`. -/ + project and `CSwL` are both on `v4.35.0`. -/ verify : Bool := false /-! ## Generated Lake project template -/ @@ -382,7 +382,7 @@ private def emitSavedImpl (config : ExtractConfig) : let buf : SaveBuffers := walkOuter width config.modPrefix text {} let toolchain ← (IO.FS.readFile "lean-toolchain").toBaseIO >>= fun | .ok s => pure s - | .error _ => pure "leanprover/lean4:v4.33.0-rc2\n" + | .error _ => pure "leanprover/lean4:v4.35.0\n" let rootFile := config.modPrefix ++ ".lean" -- Snapshot the buffer as a list, to be able to read the sources (IO) -- entry by entry. diff --git a/README.md b/README.md index 1db1376..2701b6c 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # CSwL — Computational Semantics with Lean [![License: Apache 2.0](https://img.shields.io/badge/license-Apache%202.0-blue.svg)](LICENSE) -[![Lean 4](https://img.shields.io/badge/Lean-v4.33.0-purple.svg)](https://lean-lang.org) +[![Lean 4](https://img.shields.io/badge/Lean-v4.35.0-purple.svg)](https://lean-lang.org) [![Try it live](https://img.shields.io/badge/live.lean--lang.org-try%20it-orange)](https://live.lean-lang.org/) A [Lean 4](https://lean-lang.org) adaptation of *Computational Semantics with diff --git a/lake-manifest.json b/lake-manifest.json index 2f0d8b5..e7630be 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,51 +1,51 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "aceca4eeb5a79092eabefaa75fcb72b701d02205", + "rev": "0e1ffe2e4ba5ecfdfaf15c65b8d3805dbb7134ae", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "4ac03644305a17f32139766b9ceb625ad046b85e", + "rev": "304b8561790c50222551c937ce02928df0d5b445", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "4ac03644305a17f32139766b9ceb625ad046b85e", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/cslib", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "3951377e5a3f5772737f11cd62bc5bb6a72f95d1", + "rev": "5b56df99362532c46e1175381fbbdd755bd56030", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "3951377e5a3f5772737f11cd62bc5bb6a72f95d1", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "4a174c490d8707121c4a9290800489f105d85e07", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6168b7549738a19bc837a1625c60c5d1e5dd8aeb", + "rev": "4ed2f27ecf81792abc8ff848670ac4356d0c4794", "name": "leansqlite", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,17 +125,17 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.35.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "37e7d8cb7316a88cd3e91208385c9ec6ae780019", + "rev": "6e48acac3a91665fcdc4a20d50b7ce6b7b41711f", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -145,7 +145,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "852edafa268eb038a7158551fd580ee8433847b0", + "rev": "876b844aa52183cbcc0d82fdd4d1fc349f0dac34", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -165,7 +165,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "006dc1d1db18c5dc73d637c926cf132e88df05b5", + "rev": "f77493ba242e94f518b125ef2e538cd4ab0ca678", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -175,7 +175,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4343da18d95390b09fde98efb18125677c4b500c", + "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index d6a834a..cfbdd9e 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -90,8 +90,8 @@ root = "Main" # Builds the book: `lake exe cswl-book ` writes # `_out//{html,lean}`. Use the `Makefile` (`make student`, ...). -# `lean4-autograder-main` does NOT go here on purpose: it requires the -# `v4.33.0` toolchain and collides with the Mathlib that `cslib` brings +# `lean4-autograder-main` does NOT go here on purpose: it is pinned to +# the `v4.33.0` toolchain and collides with the Mathlib that `cslib` brings # (measured: breaks `lake exe cache get`). It is a dependency only of the # standalone Lake project that `CSwLMeta/Save/Project.lean` generates under # `_out/grading/lean/`. @@ -103,13 +103,12 @@ leanOptions = {doc.verso = false} # infrastructure, like the `CSwLMeta` lib # Revision pinned for the same reason as `verso` and `doc-gen4` below: # without `rev`, the `[[require]]` followed `main`, and any `lake update` # drags the project's toolchain to whatever `cslib`'s `main` requires at -# that moment (happened on 08/14: it moved to `v4.34.0-rc1`). This is the -# revision `lake-manifest.json` already resolved to -- pinning it changes -# nothing about what compiles today. +# that moment (happened on 08/14: it moved to `v4.34.0-rc1`). Pinned to +# the release tag that matches our `lean-toolchain`, like the other three. [[require]] name = "cslib" scope = "leanprover" -rev = "3951377e5a3f5772737f11cd62bc5bb6a72f95d1" +rev = "v4.35.0" # Verso: generates the book's web (HTML) version, `Manual` genre # (`Book.lean`, target `lake exe cswl-book ` -- see `Makefile`) @@ -117,11 +116,11 @@ rev = "3951377e5a3f5772737f11cd62bc5bb6a72f95d1" # (`verso-serve.toml`). The `Literate` genre (`:literateHtml`, # `build-web.sh`) was retired on 08/16. # Revision pinned because verso's `lean-toolchain` has to match ours -# (v4.33.0-rc2); `main` may move ahead to a newer toolchain. +# (v4.35.0); `main` may move ahead to a newer toolchain. [[require]] name = "verso" git = "https://github.com/leanprover/verso" -rev = "4ac03644305a17f32139766b9ceb625ad046b85e" +rev = "v4.35.0" # doc-gen4: generates the API documentation (the reference: one HTML page # per declaration, with type, docstring, and links). Target: `lake build @@ -146,12 +145,12 @@ rev = "4ac03644305a17f32139766b9ceb625ad046b85e" # requested. # # Revision pinned to the tag that matches our `lean-toolchain` -# (v4.33.0-rc2). Being unconditional, a broken `main` would break +# (v4.35.0). Being unconditional, a broken `main` would break # everyone's build. [[require]] name = "doc-gen4" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.33.0" +rev = "v4.35.0" # Mathlib already comes in transitively via `cslib`, but without a direct # `[[require]]` here Lake does not prioritize Mathlib's version choices for @@ -162,4 +161,4 @@ rev = "v4.33.0" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "db584cd6d46c92f209a44c0f1c829460d327499d" +rev = "v4.35.0" diff --git a/lean-toolchain b/lean-toolchain index 025e595..a6aff06 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.35.0