[Merged by Bors] - feat: the longFile linter by adomani · Pull Request #15610 · leanprover-community/mathlib4

adomani · 2024-08-08T09:35:21Z

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines
(1500 by default). A value of 0 silences the linter entirely.

This PR also modifies the TextBased fileTooLong linter: now it only lints files that do not contain set_option linter.style.longFile , and removes the exceptions that are now covered by the "longFile" linter.

The TextBased longFile linter stays (for now), though it is going to be removed soon.

Once #15845 lands, the text-based linter can be removed.

I tried setting the default option for the linter to 0 and then modifying it in the lakefile to be 1500 for Mathlib, but I could not get it to work.

github-actions · 2024-08-08T09:36:07Z

PR summary c01109e5bb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ longFileLinter

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.

…inter

adomani · 2024-08-08T21:10:34Z

What I feel is really missing for this linter is a test. However, I do not know how to test it, since eoi is not a "normal" syntax node and #guard_msgs in does not latch onto it.

…inter

grunweg · 2024-08-10T10:51:19Z

Two quick thoughts (I can review properly next week):

can you add a comment to the text-based linter about this, including that many style exceptions are not necessary as these are managed by the syntax based linter, and why both linter will co-exist?
can you update the technical debt counter as well? Currently, it counts the number of "long file" style exceptions; can you ensure to also count the number of "set_option linter.longFile" (and add these... if a shell script allows this)?
as I said already: a syntax linter has much nicer user experience; thanks for upgrading the text-based linter even further!

…inter

adomani · 2024-08-11T04:09:45Z

Michael, thank you for the review!

I expanded the docs and comment to the text-based linters, mentioning the syntax one.

I also added the set_option linter.longFile count to the technical debts metrics. This is what I see locally:

$ printf '%s|%s\n' "$(
  { grep 'ERR_NUM_LIN' scripts/style-exceptions.txt
    grep '^set_option linter.longFile [0-9]*' $(git ls-files '*.lean') ; } | wc -l
)" "large files"
66|large files

and it matches the number that the Zulip post has.

grunweg

Thanks for rewriting this linter! I took the liberty to propose some wording changes directly - feel free to revert any you dislike. I have one minor comment - apart from that, this looks good to go.

Mathlib/Tactic/Linter/Lint.lean

grunweg · 2024-08-15T15:57:54Z

(Long-term, it would be nicest to have this PR remove the text-based linter instead, and import this linter in Mathlib.Init instead. We'll see in which order things land.)

…inter

Mathlib/Tactic/Linter/Lint.lean

…inter

Not recognising one is more confusing than any other behaviour. In practice, after #15610 none of these should be needed in practice.

mattrobball · 2024-08-30T08:47:22Z

bors merge

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines (1500 by default). A value of `0` silences the linter entirely. This PR also modifies the `TextBased` `fileTooLong` linter: now it only lints files that do not contain `set_option linter.style.longFile `, and removes the exceptions that are now covered by the "longFile" linter. The `TextBased` longFile linter stays (for now), though it is going to be removed soon. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

mathlib-bors · 2024-08-30T09:52:32Z

Build failed (retrying...):

Lint style

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines (1500 by default). A value of `0` silences the linter entirely. This PR also modifies the `TextBased` `fileTooLong` linter: now it only lints files that do not contain `set_option linter.style.longFile `, and removes the exceptions that are now covered by the "longFile" linter. The `TextBased` longFile linter stays (for now), though it is going to be removed soon. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

mathlib-bors · 2024-08-30T11:38:18Z

Pull request successfully merged into master.

Build succeeded:

Not recognising one is more confusing than any other behaviour. In practice, after #15610 none of these should be needed in practice.

This file has been recording exceptions to the text-based style linters in `lint-style.py` and `Linter/TextBased`. The length of this file is meant to reach zero - and now, it indeed has. 🎉 Some of the linter errors were easy to fix (and just required sustained effort), such as some misformatted author lines or missing module documentation. The main remaining entries were exceptions for the "long file linter", which has been rewritten as a syntax linter (in #15610 and #16299). Exceptions are now tracked as `set_option linter.style.longFile <number>` instead, obviating the need for this file. This implies the need for a file with transient style exceptions is gone. All of the remaining text-based linters should not be introduced in new code. For *permanent* exceptions, the file `nolints-style.txt` continues to exist; that file must (intentionally) be updated by hand. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20remove.20.60scripts.2Fstyle-exceptions.2Etxt.60)

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines (1500 by default). A value of `0` silences the linter entirely. This PR also modifies the `TextBased` `fileTooLong` linter: now it only lints files that do not contain `set_option linter.style.longFile `, and removes the exceptions that are now covered by the "longFile" linter. The `TextBased` longFile linter stays (for now), though it is going to be removed soon. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

This file has been recording exceptions to the text-based style linters in `lint-style.py` and `Linter/TextBased`. The length of this file is meant to reach zero - and now, it indeed has. 🎉 Some of the linter errors were easy to fix (and just required sustained effort), such as some misformatted author lines or missing module documentation. The main remaining entries were exceptions for the "long file linter", which has been rewritten as a syntax linter (in #15610 and #16299). Exceptions are now tracked as `set_option linter.style.longFile <number>` instead, obviating the need for this file. This implies the need for a file with transient style exceptions is gone. All of the remaining text-based linters should not be introduced in new code. For *permanent* exceptions, the file `nolints-style.txt` continues to exist; that file must (intentionally) be updated by hand. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20remove.20.60scripts.2Fstyle-exceptions.2Etxt.60)

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines (1500 by default). A value of `0` silences the linter entirely. This PR also modifies the `TextBased` `fileTooLong` linter: now it only lints files that do not contain `set_option linter.style.longFile `, and removes the exceptions that are now covered by the "longFile" linter. The `TextBased` longFile linter stays (for now), though it is going to be removed soon. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

This file has been recording exceptions to the text-based style linters in `lint-style.py` and `Linter/TextBased`. The length of this file is meant to reach zero - and now, it indeed has. 🎉 Some of the linter errors were easy to fix (and just required sustained effort), such as some misformatted author lines or missing module documentation. The main remaining entries were exceptions for the "long file linter", which has been rewritten as a syntax linter (in #15610 and #16299). Exceptions are now tracked as `set_option linter.style.longFile <number>` instead, obviating the need for this file. This implies the need for a file with transient style exceptions is gone. All of the remaining text-based linters should not be introduced in new code. For *permanent* exceptions, the file `nolints-style.txt` continues to exist; that file must (intentionally) be updated by hand. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20remove.20.60scripts.2Fstyle-exceptions.2Etxt.60)

The "longFile" linter is a syntax linter. It emits a warning on files which are longer than a certain number of lines (1500 by default). A value of `0` silences the linter entirely. This PR also modifies the `TextBased` `fileTooLong` linter: now it only lints files that do not contain `set_option linter.style.longFile `, and removes the exceptions that are now covered by the "longFile" linter. The `TextBased` longFile linter stays (for now), though it is going to be removed soon. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

This file has been recording exceptions to the text-based style linters in `lint-style.py` and `Linter/TextBased`. The length of this file is meant to reach zero - and now, it indeed has. 🎉 Some of the linter errors were easy to fix (and just required sustained effort), such as some misformatted author lines or missing module documentation. The main remaining entries were exceptions for the "long file linter", which has been rewritten as a syntax linter (in #15610 and #16299). Exceptions are now tracked as `set_option linter.style.longFile <number>` instead, obviating the need for this file. This implies the need for a file with transient style exceptions is gone. All of the remaining text-based linters should not be introduced in new code. For *permanent* exceptions, the file `nolints-style.txt` continues to exist; that file must (intentionally) be updated by hand. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20remove.20.60scripts.2Fstyle-exceptions.2Etxt.60)

adomani added 2 commits August 8, 2024 11:33

feat: the longFile linter

1a362bd

remove extra namespace

f9d236e

adomani added 10 commits August 8, 2024 13:56

add exceptions

e6cc15b

only parse the end of input and suggest standard lengths

1db59db

unlint Mathlib

1398fbf

only suggest to decrease the limit if it is off by over 200 lines

e9183ca

Fix one length

d589253

remove text-based exceptions

d99b04f

adapt exceptions

528a15c

Merge remote-tracking branch 'origin/master' into adomani/long_file_l…

4bcb4e3

…inter

yet another

8d28a85

move set_options at the end of the file

d0cc355

adomani added the t-linter Linter label Aug 8, 2024

touch ups

ea8a466

Merge remote-tracking branch 'origin/master' into adomani/long_file_l…

9e129c3

…inter

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 10, 2024

adomani added 3 commits August 11, 2024 06:03

docs for text-based linter mentioning the longFile linter

6fc990f

technical debts counts tracks both text-based and longFile linters

16794eb

Merge remote-tracking branch 'origin/master' into adomani/long_file_l…

3eabfbb

…inter

adomani removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 11, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 12, 2024

Tweak wording and documentation.

ba74595

grunweg reviewed Aug 15, 2024

View reviewed changes

Mathlib/Tactic/Linter/Lint.lean Show resolved Hide resolved

Mathlib/Tactic/Linter/Lint.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/Linter/Lint.lean Outdated Show resolved Hide resolved

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 15, 2024

Merge remote-tracking branch 'origin/master' into adomani/long_file_l…

78399cf

…inter

mattrobball reviewed Aug 29, 2024

View reviewed changes

Mathlib/Tactic/Linter/Lint.lean Show resolved Hide resolved

Mathlib/Tactic/Linter/Lint.lean Outdated Show resolved Hide resolved

adomani and others added 6 commits August 29, 2024 22:39

remove unreachable cases

5883226

Merge remote-tracking branch 'origin/master' into adomani/long_file_l…

c830787

…inter

Merge branch 'master' into adomani/long_file_linter

9940570

fix style exceptions?

74a815f

Style error is fixed on master.

fdb3d37

Merge branch 'master' into adomani/long_file_linter

c01109e

grunweg added a commit that referenced this pull request Aug 30, 2024

fix(lint-stype.py): recognise all kinds of style exceptions

35b62b7

Not recognising one is more confusing than any other behaviour. In practice, after #15610 none of these should be needed in practice.

This was referenced Aug 30, 2024

[Merged by Bors] - fix(lint-style.py): recognise all kinds of style exceptions #16297

Closed

[Merged by Bors] - chore: remove the text-based long file linter #16299

Closed

github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 30, 2024

mathlib-bors bot changed the title ~~feat: the longFile linter~~ [Merged by Bors] - feat: the longFile linter Aug 30, 2024

mathlib-bors bot closed this Aug 30, 2024

mathlib-bors bot deleted the adomani/long_file_linter branch August 30, 2024 11:38

grunweg added a commit that referenced this pull request Aug 30, 2024

fix(lint-stype.py): recognise all kinds of style exceptions

0c387bc

Not recognising one is more confusing than any other behaviour. In practice, after #15610 none of these should be needed in practice.

Parcly-Taxel mentioned this pull request Sep 1, 2024

[Merged by Bors] - feat(NumberTheory/LSeries): analytic continuation of Dirichlet L-series #13997

Closed

2 tasks

grunweg mentioned this pull request Sep 3, 2024

[Merged by Bors] - chore: remove style-exceptions.txt #16417

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: the longFile linter#15610

[Merged by Bors] - feat: the longFile linter#15610
adomani wants to merge 55 commits intomasterfrom
adomani/long_file_linter

adomani commented Aug 8, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Aug 8, 2024 •

edited

Loading

Uh oh!

adomani commented Aug 8, 2024

Uh oh!

grunweg commented Aug 10, 2024

Uh oh!

adomani commented Aug 11, 2024

Uh oh!

grunweg left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Aug 15, 2024

Uh oh!

Uh oh!

Uh oh!

mattrobball commented Aug 30, 2024

Uh oh!

mathlib-bors bot commented Aug 30, 2024

Uh oh!

mathlib-bors bot commented Aug 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

adomani commented Aug 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c01109e5bb

Import changes for modified files

Declarations diff

Uh oh!

adomani commented Aug 8, 2024

Uh oh!

grunweg commented Aug 10, 2024

Uh oh!

adomani commented Aug 11, 2024

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Aug 15, 2024

Uh oh!

Uh oh!

Uh oh!

mattrobball commented Aug 30, 2024

Uh oh!

mathlib-bors bot commented Aug 30, 2024

Uh oh!

mathlib-bors bot commented Aug 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

adomani commented Aug 8, 2024 •

edited

Loading

github-actions bot commented Aug 8, 2024 •

edited

Loading