From 393fe87b03de729cb0d380345f768c3eb8eb52dd Mon Sep 17 00:00:00 2001 From: Jason Reed Date: Tue, 25 Nov 2025 13:45:44 -0500 Subject: [PATCH] chore: update to lean v4.26.rc1 and latest verso --- book/.verso/verso-xref-manifest.json | 3 +- book/FPLean/Examples.lean | 36 ++++++++++++------------ book/FPLean/Examples/Commands/ShLex.lean | 8 +++--- book/Main.lean | 2 +- book/lake-manifest.json | 16 +++++++++-- book/lean-toolchain | 2 +- 6 files changed, 38 insertions(+), 29 deletions(-) diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json index cf2f25c..d927854 100644 --- a/book/.verso/verso-xref-manifest.json +++ b/book/.verso/verso-xref-manifest.json @@ -1,8 +1,7 @@ {"version": 0, "sources": {"manual": - {"updated": "2025-10-23:16:40:12.244921000", - "updateFrequency": "manual", + {"updateFrequency": "manual", "shortName": "ref", "root": "https://lean-lang.org/doc/reference/4.23.0/", "longName": "Lean Language Reference"}}, diff --git a/book/FPLean/Examples.lean b/book/FPLean/Examples.lean index 418add1..2c11473 100644 --- a/book/FPLean/Examples.lean +++ b/book/FPLean/Examples.lean @@ -383,17 +383,17 @@ private def quoteCode (str : String) : String := Id.run do let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str let mut n := 1 let mut run := none - let mut iter := str.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := str.startValidPos + while h : iter ≠ str.endValidPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then if k > n then n := k run := none - let delim := String.mk (List.replicate n '`') + let delim := String.ofList (List.replicate n '`') return delim ++ str ++ delim @@ -469,10 +469,10 @@ where delims : String := Id.run do let mut n := 3 let mut run := none - let mut iter := newContents.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := newContents.startValidPos + while h : iter ≠ newContents.endValidPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then @@ -927,17 +927,17 @@ where let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str let mut n := 1 let mut run := none - let mut iter := str.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := str.startValidPos + while h : iter ≠ str.endValidPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then if k > n then n := k run := none - let delim := String.mk (List.replicate n '`') + let delim := String.ofList (List.replicate n '`') return delim ++ str ++ delim macro_rules @@ -956,19 +956,19 @@ macro_rules def hasSubstring (s pattern : String) : Bool := - if h : pattern.endPos.1 = 0 then false + if h : pattern.rawEndPos.1 = 0 then false else have hPatt := Nat.zero_lt_of_ne_zero h let rec loop (pos : String.Pos.Raw) := - if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then + if h : pos.byteIdx + pattern.rawEndPos.byteIdx > s.rawEndPos.byteIdx then false else have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h) - if pos.substrEq s pattern 0 pattern.endPos.byteIdx then + if pos.substrEq s pattern 0 pattern.rawEndPos.byteIdx then have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _) true else have := Nat.sub_lt_sub_left this (pos.byteIdx_lt_byteIdx_next s) loop (pos.next s) - termination_by s.endPos.1 - pos.1 + termination_by s.rawEndPos.1 - pos.1 loop 0 diff --git a/book/FPLean/Examples/Commands/ShLex.lean b/book/FPLean/Examples/Commands/ShLex.lean index 4bdcf4e..bff7f34 100644 --- a/book/FPLean/Examples/Commands/ShLex.lean +++ b/book/FPLean/Examples/Commands/ShLex.lean @@ -8,12 +8,12 @@ private inductive State where def shlex (cmd : String) : Except String (Array String) := do let mut state : State := .normal - let mut iter := cmd.iter + let mut iter := cmd.startValidPos let mut out : Array String := #[] let mut current : Option String := none - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next' h + while h : iter ≠ cmd.endValidPos do + let c := iter.get h + iter := iter.next h match state, c with | .normal, '\\' => state := .escaped state diff --git a/book/Main.lean b/book/Main.lean index 2b46ae4..3856580 100644 --- a/book/Main.lean +++ b/book/Main.lean @@ -16,7 +16,7 @@ def config : Config where emitHtmlMulti := true htmlDepth := 2 extraFiles := [("static", "static")] - extraCss := [ + extraCss := Std.HashSet.ofList [ "/static/theme.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", diff --git a/book/lake-manifest.json b/book/lake-manifest.json index 132d071..b2d4b7c 100644 --- a/book/lake-manifest.json +++ b/book/lake-manifest.json @@ -5,17 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b1cdd66be1f055926796aa804fdc13c9e9ac17c6", + "rev": "c5f95b7296ee0d6ecfadd346c457e75cb838e853", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "66aefec2852d3e229517694e642659f316576591", + "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "57f4e6c99a4132d54a2105dec21c2e3c2af98b15", + "rev": "519b262cfc93634f904c9fb0992a45377ee49a9d", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/book/lean-toolchain b/book/lean-toolchain index 137937a..7035713 100644 --- a/book/lean-toolchain +++ b/book/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0-rc2 \ No newline at end of file +leanprover/lean4:v4.26.0-rc2 \ No newline at end of file