nolints.json file

Stream: mathlib4

[Michael Rothgang]

Seeing that style-exceptions.txt wasn't updated in some time (see other thread), I was wondering about nolints.js. Specifically,

• is this file ever automatically updated? The last ~five modifications coincide with renamings; I can imagine the author just renaming these manually. (I know mathlib3 had a bot for this; I don't know if this has been ported.)

• how can I manually update the file?
  I tried runninglake exe runLinter Mathlib; this ran for a while and then remove all entries (which is clearly not correct).

• is there a way to only run some lints, e.g. just the docBlame linter? (A pointer to the docs is sufficient.)

[Eric Wieser]

In mathlib3 we had a bot that ran nightly to auto-update this

[Mario Carneiro]

lake exe runLinter Mathlib --update is supposed to update the file

[Michael Rothgang]

(It should be lake exe runLinter --update Mathlib.)

[Michael Rothgang]

Trying that now... update: it worked (and took ages).

[Michael Rothgang]

Is there a way to run only some lints locally? lake exe runLinter --help is not helpful.

[Michael Rothgang]

Files #9832 with the new output. Quite a few changes; I commented on the PR.

[Eric Wieser]

I don't understand how the file could have grown; if there are new lint errors, CI should have failed

[Pietro Monticone]

Opened PR #11894 resolving nolints by adding docstrings for CommRing and CommSemiring.

[Michael Rothgang]

#11904 regenerates the file, removing ~20 entries which were fixed in the meantime.

[Michael Rothgang]

And #11905 removes about 60a hundred entries by tagging the respective declarations with @[inherit_doc] (and/or reformatting doc comments).

[Pietro Monticone]

I will try to tackle the remaining docBlames in the coming days / weeks.

[Michael Rothgang]

For some long-hanging fruit, NumberTheory/Dioph has about 15 scoped notations whose underlying definitions are not yet documented --- this would remove further ~30 lines from nolints.

[Yaël Dillies]

I think NumberTheory.Dioph should just be fully rewritten. It does a bunch of things in an ad hoc way because it was written before the corresponding more general theory came to mathlib

[Michael Rothgang]

Some time ago, I took a look at the remaining entries:
unfortunately, the assertion "lots of missing entries were just lost during the port (such as from ad-hoc ported files)" is mostly false. From a fraction I have examined (perhaps a third of all entries),

• about a hundred were either for deprecated items (which will be removed eventually) or referring to material in the Init folder (which is, when not deprecated, mostly cruft that probably will get removed long-term).
• most other entries are also missing in mathlib3: the Lean 4 docBlame linter also requires documentation of data fields (not proofs) of structures

[Michael Rothgang]

I filed a few PRs documenting perhaps a hundred entries: the first have been merged; still up for review are

• #12482: in Geometry, sans algebraic geometry
• #12480: in Computability
• #9827 is delegated, with all comments addressed, and (imho) just needs somebody to push the "merge" button