[Merged by Bors] - feat: unrestricted character set in unicode linter

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) 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) 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ₙ

Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean

@@ -186,10 +186,19 @@ public def emojis : 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:
 - certain ASCII characters
+- 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`)
 
@@ -202,6 +211,7 @@ public def isAllowedCharacter (c : Char) : Bool :=
   || othersInMathlib.contains c
   || emojis.contains c
   || nonEmojis.contains c
+  || unrestricted.contains c
   || c == UnicodeVariant.emoji
   || c == UnicodeVariant.text
 

MathlibTest/Linter/TextBased.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 -/