[Merged by Bors] - feat: `unrestricted` character set in unicode linter by thorimur · Pull Request #39796 · leanprover-community/mathlib4

thorimur · 2026-05-25T00:11:45Z

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 #38126.

github-actions · 2026-05-25T00:13:02Z

PR summary 5f7a90dd94

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ unrestricted

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

grunweg · 2026-05-25T08:49:43Z

Thanks for the fix! Can you update the PR description to say what maybeEmojis does (right now, you have to read the diff... which is not ideal). With that, I'm happy to maintainer merge.

adomasbaliuka · 2026-05-25T10:01:49Z

The current status is that maybeEmojis can be followed by either selector, as well as no selector (right?). Wouldn't we want to enforce that some selector is used?

thorimur · 2026-05-25T11:15:21Z

The current status is that maybeEmojis can be followed by either selector, as well as no selector (right?). Wouldn't we want to enforce that some selector is used?

I was uncertain about this, thanks for bringing it up. :) The issue is that neither the keyboard shortcut \warning for ⚠ nor the lake output including ⚠ actually includes the text selector. (Nor is it present in the mathlib python scripts that use it.) So I'm not sure if the text selector should be introduced in those places, or if the intended meaning there is in fact "let the renderer decide".

adomasbaliuka · 2026-05-25T11:30:50Z

Let's also ask our expert on Unicode variant selectors @joneugster
My understanding was that we want selectors everywhere, following arguments in, e.g., leanprover/lean4#5015

thorimur · 2026-05-25T11:40:21Z

Sounds good, let's wait for him. :) I'll also mention this zulip thread I started in case we want further discussion on this specific issue, as well as the zulip thread mentioned in the RFC for convenience.

joneugster

Looks reasonable to lift restrictions on certain characters, thanks!

joneugster · 2026-05-26T16:10:40Z

 ]

+/-- Unicode symbols in mathlib that have no restrictions on which selector they are followed by. -/
+public def maybeEmojis : Array Char := #[


so these are allowed to have either variant-selector (text/emoji) or none at all, aren't they?

maybe there is a better name for it? somehow the name suggests to me that it must have a selector, but it's optional which one.

Docstring might need to reflect that "no selector" is allowed, too.

Hmm, maybe unrestricted or unrestrictedChars?

I've tried out unrestricted (and moved it down below, since now it's not emoji-related per se), let me know what you think :)

looks good imo

joneugster · 2026-05-26T16:30:10Z

Let's also ask our expert on Unicode variant selectors @joneugster My understanding was that we want selectors everywhere, following arguments in, e.g., leanprover/lean4#5015

Variant selector do make it easier to display emojis correctly. However, adding them might potentially also bring other issues and might not be worth the time for lean4 core. Especially, what lean4 does is outside our reach (as mathlib contributors) and we should work with what we get from core.

joneugster

There is a test file which tests that emojis and non-emojis have an empty intersection. Could you add two more tests ensuring this for the new unrestricted

joneugster

Thanks!

maintainer merge

thorimur · 2026-05-26T19:12:17Z

Hmm, weird that maintainer merge did not apply the label here...maybe because github identified a merge conflict when it was applied? MathlibTest/LintStyle.lean was renamed to MathlibTest/TextBased.lean, and github said I must resolve these changes. Though, git merge upstream/master did not force me to resolve any conflict, which is maybe why merge-conflict did not get applied... 🤔 Strange.

grunweg · 2026-05-26T19:25:17Z

Let me merge this PR, then the above issue is moot :-)
Seriously: we have several reviewers agreeing on this change being desirable (I concur); the implementation looks good to me, and this is blocking another linter - let's get this in. Thanks for addressing this!
bors merge

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 #38126.

mathlib-bors · 2026-05-26T19:36:52Z

Pull request successfully merged into master.

Build succeeded:

…unity#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.

feat: create maybeEmojis, allow ⚠️

e8bc8df

thorimur marked this pull request as ready for review May 25, 2026 00:12

thorimur changed the title ~~feat: maybeEmojis and ⚠️ in unicode linter~~ feat: maybeEmojis in unicode linter May 25, 2026

github-actions Bot added the t-linter Linter label May 25, 2026

chore: finish docstring

8abe6b6

thorimur mentioned this pull request May 25, 2026

[Merged by Bors] - feat: overlapping instances linter #38126

Closed

3 tasks

JovanGerb requested a review from adomasbaliuka May 25, 2026 02:22

grunweg reviewed May 25, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean Outdated

chore: update isAllowedCharacter docstring

657e8f9

mathlib-triage Bot assigned JovanGerb May 26, 2026

JovanGerb removed their assignment May 26, 2026

joneugster reviewed May 26, 2026

View reviewed changes

chore: maybeEmojis -> unrestricted

c5f585c

joneugster reviewed May 26, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/TextBased.lean Outdated

chore: update docstring

a983bcf

thorimur changed the title ~~feat: maybeEmojis in unicode linter~~ feat: unrestricted character set in unicode linter May 26, 2026

joneugster self-assigned this May 26, 2026

joneugster reviewed May 26, 2026

View reviewed changes

chore: update tests

12a28f3

joneugster approved these changes May 26, 2026

View reviewed changes

Merge remote-tracking branch 'upstream/master' into caution-emoji-maybe

5f7a90d

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 26, 2026

mathlib-bors Bot changed the title ~~feat: unrestricted character set in unicode linter~~ [Merged by Bors] - feat: unrestricted character set in unicode linter May 26, 2026

mathlib-bors Bot closed this May 26, 2026

Uh oh!

Conversation

thorimur commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5f7a90dd94

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

grunweg commented May 25, 2026

Uh oh!

adomasbaliuka commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

adomasbaliuka commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

joneugster May 26, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur May 26, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur May 26, 2026

Choose a reason for hiding this comment

Uh oh!

joneugster May 26, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

joneugster commented May 26, 2026

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

thorimur commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented May 26, 2026

Uh oh!

mathlib-bors Bot commented May 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

thorimur commented May 25, 2026 •

edited

Loading

github-actions Bot commented May 25, 2026 •

edited

Loading

adomasbaliuka commented May 25, 2026 •

edited

Loading

thorimur commented May 25, 2026 •

edited

Loading

adomasbaliuka commented May 25, 2026 •

edited

Loading

thorimur commented May 25, 2026 •

edited

Loading

thorimur commented May 26, 2026 •

edited

Loading