From e8bc8dfdc7a516d2f45be87143b4e44a46d9a9db Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sun, 24 May 2026 19:58:41 -0400 Subject: [PATCH 1/6] =?UTF-8?q?feat:=20create=20`maybeEmojis`,=20allow=20?= =?UTF-8?q?=E2=9A=A0=EF=B8=8F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Tactic/Linter/TextBased.lean | 4 ++-- Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 1e98722a0e0929..2eefd87b6aea6a 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -361,11 +361,11 @@ def findBadUnicodeAux (s : String) (pos : s.Pos) (c : Char) if ! isAllowedCharacter c then -- bad: character not allowed. findBadUnicodeAux s posₙ cₙ (err.push (.unwantedUnicode c)) - else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) then + else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) && !(maybeEmojis.contains c) then -- bad: unwanted emoji variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ - else if cₙ == UnicodeVariant.text && !(nonEmojis.contains c) then + else if cₙ == UnicodeVariant.text && !(nonEmojis.contains c) && !(maybeEmojis.contains c) then -- bad: unwanted text variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index b4b7a8b9e8c9e3..94c1bfcac959b8 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -183,6 +183,11 @@ public def emojis : Array Char := #[ .ofNat 0x1F3C1 -- 🏁️ ] +/-- Unicode symbols in mathlib that may be followed -/ +public def maybeEmojis : Array Char := #[ + '⚠' -- ⚠️ +] + /-- Unicode symbols in mathlib that should always be followed by the text variant selector. -/ public def nonEmojis : Array Char := #[] @@ -201,6 +206,7 @@ public def isAllowedCharacter (c : Char) : Bool := || withVSCodeAbbrev.contains c || othersInMathlib.contains c || emojis.contains c + || maybeEmojis.contains c || nonEmojis.contains c || c == UnicodeVariant.emoji || c == UnicodeVariant.text From 8abe6b6238ada1c59923be5a7f19d5971930adcb Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sun, 24 May 2026 21:25:12 -0400 Subject: [PATCH 2/6] chore: finish docstring --- Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index 94c1bfcac959b8..a4205f977af12d 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -183,7 +183,7 @@ public def emojis : Array Char := #[ .ofNat 0x1F3C1 -- 🏁️ ] -/-- Unicode symbols in mathlib that may be followed -/ +/-- Unicode symbols in mathlib that have no restrictions on which selector they are followed by. -/ public def maybeEmojis : Array Char := #[ '⚠' -- ⚠️ ] From 657e8f98eb95e279ea667dc5c57eabd8fc1d9df9 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 25 May 2026 07:24:27 -0400 Subject: [PATCH 3/6] chore: update `isAllowedCharacter` docstring --- Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index a4205f977af12d..1ae814f9e32f0f 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -195,6 +195,8 @@ public def nonEmojis : Array Char := #[] Implemented using an allowlist consisting of: - certain ASCII characters +- certain emojis (`emojis` and `maybeEmojis`) +- certain non-emoji variants of emojifiable characters (`nonEmojis` and `maybeEmojis`) - characters with abbreviations in the VSCode extension (`withVSCodeAbbrev`) - "the rest" (`othersInMathlib`) From c5f585c3fc6e8f243213addfee041659947def12 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 26 May 2026 12:22:15 -0400 Subject: [PATCH 4/6] chore: `maybeEmojis` -> `unrestricted` --- Mathlib/Tactic/Linter/TextBased.lean | 6 ++++-- Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean | 13 +++++++------ 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 2eefd87b6aea6a..56ffb83a679f78 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -361,11 +361,13 @@ def findBadUnicodeAux (s : String) (pos : s.Pos) (c : Char) if ! isAllowedCharacter c then -- bad: character not allowed. findBadUnicodeAux s posₙ cₙ (err.push (.unwantedUnicode c)) - else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) && !(maybeEmojis.contains c) then + else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) && !(unrestricted.contains c) then -- bad: unwanted emoji variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ - else if cₙ == UnicodeVariant.text && !(nonEmojis.contains c) && !(maybeEmojis.contains c) then + else if + cₙ == UnicodeVariant.text && !(nonEmojis.contains c) && !(unrestricted.contains c) + then -- bad: unwanted text variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index 1ae814f9e32f0f..34a3d45df58d47 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -183,14 +183,15 @@ public def emojis : Array Char := #[ .ofNat 0x1F3C1 -- 🏁️ ] -/-- Unicode symbols in mathlib that have no restrictions on which selector they are followed by. -/ -public def maybeEmojis : Array Char := #[ - '⚠' -- ⚠️ -] - /-- Unicode symbols in mathlib that should always be followed by the text variant selector. -/ public def nonEmojis : Array Char := #[] +/-- Unicode symbols in mathlib that have no restrictions on whether they are followed by a selector +or which selector they are followed by. -/ +public def unrestricted : Array Char := #[ + '⚠' -- ⚠️, ⚠. Lake output uses '⚠' and does not include the text selector. +] + /-- If `false`, the character is not allowed in Mathlib. Implemented using an allowlist consisting of: @@ -208,8 +209,8 @@ public def isAllowedCharacter (c : Char) : Bool := || withVSCodeAbbrev.contains c || othersInMathlib.contains c || emojis.contains c - || maybeEmojis.contains c || nonEmojis.contains c + || unrestricted.contains c || c == UnicodeVariant.emoji || c == UnicodeVariant.text From a983bcf04c7c98a40337dd26eab90b7c2f167e71 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 26 May 2026 12:23:41 -0400 Subject: [PATCH 5/6] chore: update docstring --- Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index 34a3d45df58d47..560c29f09cb792 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -196,8 +196,9 @@ public def unrestricted : Array Char := #[ Implemented using an allowlist consisting of: - certain ASCII characters -- certain emojis (`emojis` and `maybeEmojis`) -- certain non-emoji variants of emojifiable characters (`nonEmojis` and `maybeEmojis`) +- certain emojis (`emojis`) +- certain non-emoji variants of emojifiable characters (`nonEmojis`) +- certain characters with no selector restrictions (`unrestricted`) - characters with abbreviations in the VSCode extension (`withVSCodeAbbrev`) - "the rest" (`othersInMathlib`) From 12a28f321eca92aa74e40c6e54a4abd8d5a6dd4d Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 26 May 2026 12:38:27 -0400 Subject: [PATCH 6/6] chore: update tests --- MathlibTest/LintStyle.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/MathlibTest/LintStyle.lean b/MathlibTest/LintStyle.lean index 1f3b696f653e86..18b54249b9caa9 100644 --- a/MathlibTest/LintStyle.lean +++ b/MathlibTest/LintStyle.lean @@ -665,14 +665,21 @@ open Mathlib.Linter.TextBased.UnicodeLinter /- A character either does or doesn't have an abbreviation in the VSCode extension. -/ #guard withVSCodeAbbrev.toList ∩ othersInMathlib.toList = ∅ -/- A character either is or isn't an emoji. -/ +/- No character is both an emoji and not an emoji. -/ #guard emojis.toList ∩ nonEmojis.toList = ∅ +/- No character is both an emoji and unrestricted. -/ +#guard emojis.toList ∩ unrestricted.toList = ∅ + +/- No character is both a non-emoji and unrestricted. -/ +#guard nonEmojis.toList ∩ unrestricted.toList = ∅ + def allLinterDefinedCharacterLists : List (List Char) := [ withVSCodeAbbrev, othersInMathlib, emojis, - nonEmojis + nonEmojis, + unrestricted ].map Array.toList /- Ensure none of the lists contain duplicates -/