global notation linter

Stream: mathlib4

[Patrick Massot]

Should we have a linter against global notation? Of course it could be deactivated when needed. I just found #10043 that introduced an extremely generic notation (the infix operator ^*) to use it exactly twice in Mathlib if I’m not mistaken. Clearly this is a failure of the reviewing process but linters should be here to help reviewers.

[Patrick Massot]

We’ll see in #13518 whether CI agrees this notation was not used elsewhere.

[Yaël Dillies]

I mean surely global notation is usually fine?

[Patrick Massot]

Maybe there would be too many nolints. I’m really not sure what to do. Maybe we need some GitHub bot to detect that word notation and post a message reminding reviewers to check whether the notation is global and reasonable.

[Patrick Massot]

In the mean time CI confirmed that global ^* was used exactly twice in Mathlib. I would appreciate a quick merge of #13518 so that I can finish updating GlimpseOfLean.

[Richard Osborn]

I do think in general it would be nice for CI to post a summary of a PR. A list of theorems added and/or deleted, notations added, change in the import graph, etc... Basically, anything that would make it easier for reviewers to spot suspicious changes.

[Patrick Massot]

@Alex J. Best had a nice prototype in January.

[Damiano Testa]

Richard Osborn said:

I do think in general it would be nice for CI to post a summary of a PR. A list of theorems added and/or deleted, notations added, change in the import graph, etc... Basically, anything that would make it easier for reviewers to spot suspicious changes.

Each PR has a CI step called summarize-declarations that does a part of that.

A more verbose output, such as this and a more compact one that you can get by adding the label move-decls (the same PR as an example).

[Alex J. Best]

Patrick Massot said:

Alex J. Best had a nice prototype in January.

I would even say that it was progressing beyond the prototype stage. But I no longer have time to work on it. If anyone, or the community wants to adopt github.com/alexjbest/leaff that would make me very happy

[Yaël Dillies]

Speaking of PRs introducing global notation... #11142

[Patrick Massot]

Thanks for noticing. All those notations should definitely be scoped.

[Patrick Massot]

Once again, I suffering because of crazy global notations introduced in super low-level files. Today it’s https://github.com/leanprover-community/mathlib4/blob/d4a7b67c52e526f04082b832d2f3d298b17bd29e/Mathlib/Logic/Function/Defs.lean#L46-L47. @Kyle Miller is there anything I can do to deactivate this notation in a downstream project? Or should I stick to Lean 4.15.0 because of this?

[Yaël Dillies]

I don't understand why 4.15.0 vs 4.16.0-rc1 would change anything. This notation has been around forever (and is quite useless, I agree)

[Kyle Miller]

My understanding is that you can't disable syntaxes.

I don't understand why 4.15->4.16 would change anything either.

Given that this is a mathlib notation, could we scope it (or delete it?)

[Yaël Dillies]

Happy to see it go to :wastebasket:

[Eric Wieser]

I think it's used fairly heavily with Disjoint (f on tuple) and Pairwise (Disjoint on tuple); but maybe f.on tuple would be fine instead

[Patrick Massot]

Yaël, the reason why 4.15.0 vs 4.16.0-rc1 changes everything has been discussed at length already, it’s lean4#6012.

[Yaël Dillies]

Ah! not because the mathlib on notation but because your on notation changed.

[Patrick Massot]

This major change in parsing makes it much harder to avoid hitting this on notation bug.

[Eric Wieser]

What prevents you using the same token?

[Eric Wieser]

(we have many notations in mathlib that use a ] token, for instance)

[Patrick Massot]

I guess it creates a grammar ambiguity.

[Patrick Massot]

By the way, I wrote the wrong number. This issue prevents bumping from 4.14.0 to 4.15.0, it has nothing to do with 4.16

[Patrick Massot]

If anyone wants to play with this, it’s at https://github.com/PatrickMassot/verbose-lean4/tree/bump

[Patrick Massot]

https://github.com/PatrickMassot/verbose-lean4/blob/bump/Verbose/French/By.lean#L8 does not work because of Mathlib’s on notation.

[Patrick Massot]

It creates tons of unexpected token 'obtient'; expected term.

[Kim Morrison]

@Patrick Massot, I'm preparing a PR to scope on. Will scoping be enough for your purposes? The Function namespace gets opened pretty frequently.

I'm also happy to require people to write f.on tuple as Eric suggested above.

[Kim Morrison]

chore: scope 'on' notation to Function #20562