From d3fc45eada25f49170f62157c95c12ca42b2f26c Mon Sep 17 00:00:00 2001 From: fgdorais <3247514+fgdorais@users.noreply.github.com> Date: Tue, 16 Dec 2025 09:05:07 +0000 Subject: [PATCH 1/6] chore: update toolchain nightly-2025-12-16 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index bd19bde0c..ea152ff02 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 +leanprover/lean4:nightly-2025-12-16 From 6a23ff40a1a7327d0ac839f7543d470d1dbe1ebf Mon Sep 17 00:00:00 2001 From: fgdorais <3247514+fgdorais@users.noreply.github.com> Date: Wed, 17 Dec 2025 09:05:21 +0000 Subject: [PATCH 2/6] chore: update toolchain nightly-2025-12-17 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index ea152ff02..105d47289 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-12-16 +leanprover/lean4:nightly-2025-12-17 From beccb9259585fc616c7f524f7a040cb74e012746 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 16 Feb 2026 08:51:54 -0500 Subject: [PATCH 3/6] fix: use String.Slice.posGT --- UnicodeBasic/CharacterDatabase.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/UnicodeBasic/CharacterDatabase.lean b/UnicodeBasic/CharacterDatabase.lean index 69a1fa786..b587127b6 100644 --- a/UnicodeBasic/CharacterDatabase.lean +++ b/UnicodeBasic/CharacterDatabase.lean @@ -39,7 +39,7 @@ def ofFile (path : System.FilePath) : IO UCDStream := protected partial def nextLine? (stream : UCDStream) : Option (String.Slice × UCDStream) := do let line := stream.trimAsciiEnd.takeWhile (.!='\n') if h : line.rawEndPos < stream.rawEndPos then - let nextPos := stream.findNextPos line.rawEndPos h + let nextPos := stream.posGT line.rawEndPos h let line := (line.takeWhile (.!='#')).trimAsciiEnd if line.isEmpty then UCDStream.nextLine? {stream with toSlice := stream.sliceFrom nextPos} From 90fcfdf4eead3d3cd9d7e77555aabdff0cee5061 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 17 Feb 2026 09:54:15 -0500 Subject: [PATCH 4/6] chore: update toolchain v4.29.0-rc1 --- UnicodeBasic/CharacterDatabase.lean | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/UnicodeBasic/CharacterDatabase.lean b/UnicodeBasic/CharacterDatabase.lean index 69a1fa786..b587127b6 100644 --- a/UnicodeBasic/CharacterDatabase.lean +++ b/UnicodeBasic/CharacterDatabase.lean @@ -39,7 +39,7 @@ def ofFile (path : System.FilePath) : IO UCDStream := protected partial def nextLine? (stream : UCDStream) : Option (String.Slice × UCDStream) := do let line := stream.trimAsciiEnd.takeWhile (.!='\n') if h : line.rawEndPos < stream.rawEndPos then - let nextPos := stream.findNextPos line.rawEndPos h + let nextPos := stream.posGT line.rawEndPos h let line := (line.takeWhile (.!='#')).trimAsciiEnd if line.isEmpty then UCDStream.nextLine? {stream with toSlice := stream.sliceFrom nextPos} diff --git a/lean-toolchain b/lean-toolchain index c248ed068..c7ad81a70 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-02-16-rev1 +leanprover/lean4:v4.29.0-rc1 From d3329d266d6a2e368b9c5eaf132e8753bcf7c7fe Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sun, 22 Mar 2026 16:04:57 -0400 Subject: [PATCH 5/6] fix: docstring edit --- UnicodeBasic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/UnicodeBasic.lean b/UnicodeBasic.lean index e6d0d91e3..b55675191 100644 --- a/UnicodeBasic.lean +++ b/UnicodeBasic.lean @@ -49,7 +49,7 @@ namespace Unicode /-- Get character name When the Unicode property `Name` is empty, a unique code label is returned - as described in Unicode Standard, section 4.8. These labels start with + as recommended in Unicode Standard, section 4.8. These labels start with `'<'` (U+003C) and end with `'>'` (U+003E) so they are distinguishable from actual name values. From 5c0bd26893a2cc797f01f073b320a9605f963fb6 Mon Sep 17 00:00:00 2001 From: fgdorais <3247514+fgdorais@users.noreply.github.com> Date: Sat, 28 Mar 2026 03:50:06 +0000 Subject: [PATCH 6/6] chore: update toolchain v4.29.0 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b222dcbd6..14791d727 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-03-25 +leanprover/lean4:v4.29.0