feat: unrestricted character set in unicode linter (leanprover-community#39796)

This PR creates the `unrestricted` array in the unicode linter, which contains characters that have no restrictions on which selector they are followed by, and are not enforced to be followed by any selector at all.

We include `'⚠'` in it to allow `⚠️`. We don't want to ban the text version (`⚠`), as this is used in lake output (without the text selector) and so may conceivably be mentioned in a comment.

We plan to use `⚠️` in leanprover-community#38126.

Author: thorimur

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 -/