feat(Tactic/Linter): lint unwanted unicode

[adomasbaliuka]

Add a text-based style linter that checks all unicode characters.

• Only allow whitelisted characters, with a suggestion to add the flagged character to the whitelist
• Some characters are specified to use emoji-variant or text-variant. The linter ensures these variant-selectors only appear in the correct places and provides an auto-fix to clean them up.

---

Discussed at Zulip

The current proposal checks each character against a whitelist. There is also the question of what the whitelist should contain.

A reasonable whitelist might be "all unicode currently in Mathlib" ∪ Wikipedia/Mathematical_operators_and_symbols_in_Unicode ∪ EdAyers/mathlib3/docs/unicode.md. Currently implemented is a subset of this list closer to what's currently present in mathlib.

• depends on: [Merged by Bors] - chore: remove non-ascii whitespace #17068
• depends on: [Merged by Bors] - fix: remove non-breaking-space #17116
• depends on: feat(Tactic/Linter): add unicode linter for unicode variant-selectors #17129 (part 1 of this PR)
• depends on: feat(Tactic/Linter): add unicode linter for unwanted characters #17131 (part 2 of this PR)
• Future note: @adomasbaliuka says: "we might add something to the Mathlib 4 docs about this as well?"

[github-actions]

PR summary 063b3b2533

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.TextBased	3	16	+13 (+433.33%)

Import changes for all files

Files	Import difference
There are 4226 files with changed transitive imports taking up over 178601 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ ASCII.allowed
+ ASCII.allowedWhitespace
+ ASCII.printable
+ UnicodeVariant.emoji
+ UnicodeVariant.text
+ emojis
+ findBadUnicode
+ findBadUnicodeAux
+ isAllowedCharacter
+ nonEmojis
+ othersInMathlib
+ printCodepointHex
+ removeQuotations
+ unicodeLinter
+ withVSCodeAbbrev

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[grunweg]

Some quick comments. Overall, this linter

• flags interesting things
• does not seem to turn up something worrying,
  both of which is great.

[grunweg]

Would you like to take a look at the "spaces" the linter flags? (I haven't checked what this is about exactly; just looking at it in the text editor is probably not useful...)

[adomasbaliuka]

Would you like to take a look at the "spaces" the linter flags? (I haven't checked what this is about exactly; just looking at it in the text editor is probably not useful...)

That seems to be

' ': Unicode U+202F (category Zs: Separator, space)

I think we'll remove them from Mathlib but let's see...

[adomasbaliuka]

I have removed all non-breaking spaces (U+00a0) from Mathlib. This might be excessive:

• I can PR it separately if the change is too big or off topic in this PR
• We may decide to allow non-breaking spaces

[grunweg]

Thank you! I think splitting the removal of non-breaking spaces into a separate PR (do you know git cherry-pick?) makes sense, and would be happy to nominate it for the maintainers to look. Reading the zulip discussion, changing the spaces does not appear controversial to me.

Update: for me, splitting the space changes is positive anyway, as it's a large enough change (200 lines), completely mechanic and very different from the rest of this PR. That would be true regardless of whether the change is controversial.

[adomasbaliuka]

@joneugster LGTM

[eric-wieser]

I think these are genuinely intended to be non-breaking; the right solution is to put this in a code block.

[joneugster]

Sorry these are about the text-variant-selector of the arrows characters, i.e. there were invisible \uFE0E following the diagonal arrows to prevent them form being displayed as emojis.

There are no spaces changed here.

If they are supposed to have the variant-selector (which is a fair choice) then, they can be added to the list of text-symbols defined here and the variant-selectors will be fixed automatically by lake exe lint-style --fix

[eric-wieser]

These are also intended to be non-breaking; I think using the unicode escape would be appropriate here.

[joneugster]

same here, there is no space change, but the magnifying glass received a emoji-variant-selector because its specified in the list of emojis.

[joneugster]

For context, there are currently no non-breaking spaces in any parts of mathlib except in docstrings about condensed mathematics & cat. theory because Dagur's IDE automatically adds them after each closing `

And the dependency PRs fixing whitespace are mainly because Dagur's quite busy and commiting a lot :D

[eric-wieser]

Let's do this with Lean!

[github-actions]

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

	'₃', '₄', '₅', '₆', '₇', '₈', '₉', '₀', '←', 'Ø', '⅋',
	'₃', '₄', '₅', '₆', '₇', '₈', '₉', '₀', '← ', 'Ø', '⅋',

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: remove non-ascii whitespace #17068
• [Merged by Bors] - fix: remove non-breaking-space #17116
• feat(Tactic/Linter): add unicode linter for unicode variant-selectors #17129
• feat(Tactic/Linter): add unicode linter for unwanted characters #17131
  By Dependent Issues (🤖). Happy coding!