feat: update toolchain

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1

Leansec/Combinators.lean

@@ -260,15 +260,14 @@ section
     def char : Char → ⟦ Parser mn ρ ρ.Tok ⟧ :=
       exact ∘ Coe.coe
 
-    def string (t : {s : String // (s.data.length ≠ 0)}) : ⟦ Parser mn ρ String ⟧ :=
-      λ {n : ℕ} =>
-      match t with
-      | ⟨⟨[]⟩, h⟩ => by contradiction
-      | ⟨⟨(x :: xs)⟩, _⟩ =>
-        mapc t.val $ exacts $ FreeSemigroup.map (↑·) ⟨x, xs⟩
+    def string (t : {s : String // s.toList.length ≠ 0}) : ⟦ Parser mn ρ String ⟧ :=
+    λ {n} =>
+      match h : t.val.toList with
+      | [] => (t.property (by simp_all [String.toList])).elim
+      | x :: xs => mapc t.val $ exacts $ FreeSemigroup.map (↑·) ⟨x, xs⟩
 
     def space : ⟦ Parser mn ρ ρ.Tok ⟧ :=
-      anyOf (Coe.coe <$> (" \t\n\r\x0c").data)
+      anyOf (Coe.coe <$> (" \t\n\r\x0c").toList)
 
     def spaces : ⟦Parser mn ρ (FreeSemigroup ρ.Tok)⟧ :=
       list1 space

Leansec/Running.lean

@@ -14,7 +14,7 @@ class Tokenizer (tok : Type) where
   lessTokens : (s : String) → (tokenize s).length ≤ s.length
 
 instance : Tokenizer Char where
-  tokenize := String.data
+  tokenize := String.toList
   lessTokens s := by constructor
 
 class SizedInput (tok : Type) (toks : Nat → Type) where

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "40e9f225b064c622d45046dd6154308d48d6d8b6",
+   "rev": "a8519e1a24e2621dd00ef149a1777293bbbd9ddb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
+   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
+   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
+   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.59",
+   "inputRev": "v0.0.82",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1",
+   "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
+   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6",
+   "rev": "f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.26.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "leansec",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc5
+leanprover/lean4:v4.26.0-rc2