[Merged by Bors] - feat: rewrite file length check in Lean by grunweg · Pull Request #13620 · leanprover-community/mathlib4

grunweg · 2024-06-07T22:17:36Z

This is the first in a series of PRs rewriting most checks from lint-style.py in Lean.
This PR sets up the basic infrastructure and ports the check for files longer than 1500 lines.
This includes parsing style-exceptions.txt.

To enable a gradual conversion of the linters, this PR adds a new executable lint_style (which runs the rewritten linters), and has lint-style.sh call this one also.

this currently reads the files to lint from {Archive,Counterexamples,Mathlib}.lean: should this traverse the file system (like mk_all) instead? My reasoning is that these files are ensured to be up-to-date in CI, so in practice this amounts to similar results --- and reading one file only is easier and slightly less I/O.

This changes the ordering of the output lines in style-exceptions.txt: the ones on the file length come last.
I think this is in fact more readable in practice, given that there are only about three kinds of style exceptions left.

github-actions · 2024-06-07T22:18:11Z

PR summary a15b10fc37

Import changes

No significant changes to the import graph

Declarations diff

+ ErrorContext
+ StyleError
+ StyleError.errorCode
+ StyleError.errorMessage
+ StyleError.normalise
+ checkFileLength
+ formatErrors
+ instance : BEq ErrorContext
+ isImportsOnlyFile
+ lintAllFiles
+ lintFile
+ main
+ outputMessage
+ parse?_errorContext
+ parseStyleExceptions

You can run this locally as follows

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

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

grunweg · 2024-06-08T15:32:46Z

Mathlib/Tactic/Linter/TextBased.lean

+/-- Create the underlying error message for a given `StyleError`. -/
+def StyleError.errorMessage (err : StyleError) : String := match err with
+  | StyleError.fileTooLong current_size size_limit =>
+      s!"{size_limit} file contains {current_size} lines, try to split it up"


For reviewers: this matches the current output of lint-style.py. #13623 will add a more human-readable variant.

grunweg · 2024-06-08T15:41:47Z

Mathlib/Tactic/Linter/TextBased.lean

+  beq ctx ctx' :=
+      -- XXX: `lint-style.py` was calling `resolve()` on the path before before comparing them
+      -- should we also do so?
+      ctx.path == ctx'.path


In my local testing, this works as-is.

Looking through this file's history, this goes back to #352. I don't see why it would be useful now. I propose to simply remove the comment and the check.

grunweg · 2024-06-08T15:42:12Z

Mathlib/Tactic/Linter/TextBased.lean

+
+/-- Output the formatted error message, containing its context. -/
+def outputMessage (errctx : ErrorContext) : String :=
+  -- We are outputting for github: duplicate file path, line number and error code,


#13623 will add human-readable output here - this PR preserves existing behaviour

Mathlib/Tactic/Linter/TextBased.lean

grunweg · 2024-06-08T15:45:18Z

Mathlib/Tactic/Linter/TextBased.lean

+      -- Omit the line number, as we don't use it anyway.
+      return (err.map fun e ↦ (ErrorContext.mk e 0 path))
+    -- XXX: print an error on any lines which don't match the particular format.
+    | _ => -- IO.println s!"Invalid input file: line {line} doesn't match any particular format"


Printing an error here doesn't work because the monads don't work out. Quickly trying to fix that failed - a suggestion is welcome.

Why not just return a fake ErrorContext here?

Sure, I could to this - but I don't see the advantage over just returning none (as I'm doing now). Can you articulate why you consider that better?

Printing an error is merely for validating the style exceptions file; I'm also fine with leaving this out: the style exceptions file is usually automatically generated, after all! (And if not, we should make updating it easier, as #13623 does.)

Okay. Do you want to just clean up the comments here, and explain the situation (maybe that it would be nice to report an error, but awkward, and hopefully because the file is automatically generated unnecessary)?

Sounds good; I added such a comment.

Mathlib/Tactic/Linter/TextBased.lean

grunweg · 2024-06-08T15:46:26Z

.github/workflows/build_fork.yml

          python-version: 3.8

-      - name: lint
+      - name: install elan


This step is necessary as the "lint style" workflow now needs lake to run lake exe lint_style.

As all module names do not contain path separators, splitting on file paths is actually fine :-)

thus, we *could* error on invalid lines, in principle.

kim-em · 2024-06-20T23:04:20Z

bors d+

mathlib-bors · 2024-06-20T23:04:22Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

grunweg · 2024-06-21T07:01:03Z

Thank you for the review!
bors r+

This is the first in a series of PRs rewriting most checks from `lint-style.py` in Lean. This PR sets up the basic infrastructure and ports the check for files longer than 1500 lines. This includes parsing `style-exceptions.txt`. To enable a gradual conversion of the linters, this PR adds a new executable `lint_style` (which runs the rewritten linters), and has `lint-style.sh` call this one also.

mathlib-bors · 2024-06-21T07:58:26Z

Pull request successfully merged into master.

Build succeeded:

…dable output by default (#14012) - Fix the output of `update-style-exceptions.py` by making `lake exe lint_style` optionally produce output in the right format: this regressed in #13620 - The current error messages are tailored for github annotations, which are not very readable for running the linter locally. Produce a human-readable and clickable error by default, but add a flag (which CI sets) for producing github-style output. This entails adding a small CLI for the lint-style executable.

This is the first in a series of PRs rewriting most checks from `lint-style.py` in Lean. This PR sets up the basic infrastructure and ports the check for files longer than 1500 lines. This includes parsing `style-exceptions.txt`. To enable a gradual conversion of the linters, this PR adds a new executable `lint_style` (which runs the rewritten linters), and has `lint-style.sh` call this one also.

…dable output by default (#14012) - Fix the output of `update-style-exceptions.py` by making `lake exe lint_style` optionally produce output in the right format: this regressed in #13620 - The current error messages are tailored for github annotations, which are not very readable for running the linter locally. Produce a human-readable and clickable error by default, but add a flag (which CI sets) for producing github-style output. This entails adding a small CLI for the lint-style executable.

This is the first in a series of PRs rewriting most checks from `lint-style.py` in Lean. This PR sets up the basic infrastructure and ports the check for files longer than 1500 lines. This includes parsing `style-exceptions.txt`. To enable a gradual conversion of the linters, this PR adds a new executable `lint_style` (which runs the rewritten linters), and has `lint-style.sh` call this one also.

…dable output by default (#14012) - Fix the output of `update-style-exceptions.py` by making `lake exe lint_style` optionally produce output in the right format: this regressed in #13620 - The current error messages are tailored for github annotations, which are not very readable for running the linter locally. Produce a human-readable and clickable error by default, but add a flag (which CI sets) for producing github-style output. This entails adding a small CLI for the lint-style executable.

grunweg added awaiting-review CI Modifies the continuous integration setup or other automation t-linter Linter tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels Jun 7, 2024

grunweg force-pushed the MR-rewrite-file-length-check branch from 6bb829f to 4a26f39 Compare June 7, 2024 22:22

grunweg mentioned this pull request Jun 8, 2024

feat: prettier output on style errors #13623

Closed

2 tasks

grunweg commented Jun 8, 2024

View reviewed changes

This was referenced Jun 10, 2024

[Merged by Bors] - feat: rewrite the copyright header check in Lean #13240

Closed

[Tracking PR] feat: rewrite most style linters in Lean #13199

Closed

grunweg added 6 commits June 15, 2024 11:46

Initial version

1d5f765

Fix style lint job.

4a4a77f

Open System; remove two other unused open's.

f99ffdd

fix: split paths in a safe way

dcfd369

As all module names do not contain path separators, splitting on file paths is actually fine :-)

style: use \centerdot for anonymous functions more

2ec13b7

Move ignoring of comments one level up:

3540df4

thus, we *could* error on invalid lines, in principle.

grunweg force-pushed the MR-rewrite-file-length-check branch from 39ba36c to 3540df4 Compare June 15, 2024 09:59

Small tweak.

f8a8161

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 Jun 19, 2024

Merge branch 'master' into MR-rewrite-file-length-check

8c831c9

grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 19, 2024

github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 20, 2024

Tweak comments.

a15b10f

grunweg mentioned this pull request Jun 21, 2024

[Merged by Bors] - feat(lint-style): fix update-style-exceptions.py; produce human-readable output by default #14012

Closed

mathlib-bors bot changed the title ~~feat: rewrite file length check in Lean~~ [Merged by Bors] - feat: rewrite file length check in Lean Jun 21, 2024

mathlib-bors bot closed this Jun 21, 2024

mathlib-bors bot deleted the MR-rewrite-file-length-check branch June 21, 2024 07:58

grunweg mentioned this pull request Jul 10, 2024

[Merged by Bors] - chore: update some style exceptions #14607

Closed

Conversation

grunweg commented Jun 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary a15b10fc37

Import changes

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kim-em commented Jun 20, 2024

Uh oh!

mathlib-bors bot commented Jun 20, 2024

Uh oh!

grunweg commented Jun 21, 2024

Uh oh!

mathlib-bors bot commented Jun 21, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

grunweg commented Jun 7, 2024 •

edited

Loading

github-actions bot commented Jun 7, 2024 •

edited

Loading