chore(deps): bump Lean toolchain and dependencies to v4.35.0

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 ≠ "")
 ```
 

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
 ```
 

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`

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.

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

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",

lakefile.toml

@@ -90,8 +90,8 @@ root = "Main"
 
 # Builds the book: `lake exe cswl-book <variant>` writes
 # `_out/<variant>/{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,25 +103,24 @@ 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 <variant>` -- see `Makefile`)
 # and the `lake exe verso-serve` that serves `_out/` locally
 # (`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"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.0
+leanprover/lean4:v4.35.0