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 01/11] 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 02/11] 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 03/11] 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 04/11] 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 05/11] 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 5785c13a0146f5f8f65febd2905546edf85871a7 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 06/11] chore: update toolchain --- lean-toolchain | 1 + 1 file changed, 1 insertion(+) diff --git a/lean-toolchain b/lean-toolchain index 2210cba4f..e7e267fe4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1,2 @@ leanprover/lean4:v4.30.0-rc1 + From 093040a01ac04173fa3e0c8e85dcbc395595806f 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 07/11] chore: update toolchain nightly-2025-12-17 --- lean-toolchain | 1 - 1 file changed, 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index e7e267fe4..2210cba4f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1,2 +1 @@ leanprover/lean4:v4.30.0-rc1 - From 62ee2f029596d089721ce1670d301ad6488170db Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 17 Feb 2026 09:54:15 -0500 Subject: [PATCH 08/11] chore: update toolchain v4.29.0-rc1 --- lean-toolchain | 1 + 1 file changed, 1 insertion(+) diff --git a/lean-toolchain b/lean-toolchain index 2210cba4f..e7e267fe4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1,2 @@ leanprover/lean4:v4.30.0-rc1 + From 79a6e460771cc4a5d5729366603d63848a6255bd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 12 Apr 2026 18:38:28 +1000 Subject: [PATCH 09/11] patch for leanprover/lean4#13372 --- UnicodeBasic/CharacterDatabase.lean | 5 ++++- lean-toolchain | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/UnicodeBasic/CharacterDatabase.lean b/UnicodeBasic/CharacterDatabase.lean index b587127b6..764867b65 100644 --- a/UnicodeBasic/CharacterDatabase.lean +++ b/UnicodeBasic/CharacterDatabase.lean @@ -15,7 +15,10 @@ namespace Unicode structure UCDStream extends String.Slice where /-- `isUnihan` is true if the records are tab separated -/ isUnihan := false -deriving Inhabited +-- deriving Inhabited -- See https://github.com/leanprover/lean4/issues/13372 + +instance : Inhabited UCDStream where + default := { toSlice := "", isUnihan := false } namespace UCDStream diff --git a/lean-toolchain b/lean-toolchain index 9187f2ebf..bca52a66f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-10 +leanprover/lean4:nightly-2026-04-11 From 4546b3e9707420c8dbaa69f2ef9b695f6e3367e8 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 14 Apr 2026 11:04:21 -0700 Subject: [PATCH 10/11] Revert patch for leanprover/lean4#13372 (#135) --- UnicodeBasic/CharacterDatabase.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/UnicodeBasic/CharacterDatabase.lean b/UnicodeBasic/CharacterDatabase.lean index 764867b65..b587127b6 100644 --- a/UnicodeBasic/CharacterDatabase.lean +++ b/UnicodeBasic/CharacterDatabase.lean @@ -15,10 +15,7 @@ namespace Unicode structure UCDStream extends String.Slice where /-- `isUnihan` is true if the records are tab separated -/ isUnihan := false --- deriving Inhabited -- See https://github.com/leanprover/lean4/issues/13372 - -instance : Inhabited UCDStream where - default := { toSlice := "", isUnihan := false } +deriving Inhabited namespace UCDStream From b9bc687feb246d1e910bd57001a5c0a64661ff79 Mon Sep 17 00:00:00 2001 From: fgdorais <3247514+fgdorais@users.noreply.github.com> Date: Fri, 17 Apr 2026 12:46:42 +0000 Subject: [PATCH 11/11] chore: update toolchain v4.30.0-rc2 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 474b1d259..6c7e31fff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-17 +leanprover/lean4:v4.30.0-rc2