[Merged by Bors] - chore: import enabled mathlib syntax linters in `Mathlib.Init` by grunweg · Pull Request #15845 · leanprover-community/mathlib4

grunweg · 2024-08-15T16:18:22Z

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file.
Hence, move them to Mathlib.Init, which has precisely this purpose.

All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default.
Linters missing from this list include

Linter/Textbased (which is not syntax-based)
Linter/MinImports (which is off by default)
Linter/HaveLet (which is disabled right now)

All linters only have imports in Lean, except for Linter/Lint (which imports Batteries.Tactic.Lint to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early.

semorrison indicated that these linters are fine to import for now.

Follow-up clean-ups, out of scope of this PR

write a linter to ensure Mathlib.Init is actually imported in every file
remove the text-based line length linter (which is now duplicate)
adapt the in-flight PR for the file length linter

github-actions · 2024-08-15T16:19:01Z

PR summary 7fb2b66537

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Util.SleepHeartbeats	2	12	+10 (+500.00%)
Mathlib.Tactic.Linter.HashCommandLinter	4	2	-2 (-50.00%)
Mathlib.Tactic.Linter.Lint	4	2	-2 (-50.00%)
Mathlib.Tactic.Linter.UnusedTactic	4	2	-2 (-50.00%)
Mathlib.Tactic.Linter.GlobalAttributeIn	3	2	-1 (-33.33%)
Mathlib.Tactic.Linter.OldObtain	3	2	-1 (-33.33%)
Mathlib.Tactic.Linter.RefineLinter	3	2	-1 (-33.33%)
Mathlib.Tactic.Linter.Style	3	2	-1 (-33.33%)
Mathlib.Tactic.Linter	15	19	+4 (+26.67%)
Mathlib.Tactic.Subsingleton	50	57	+7 (+14.00%)

Import changes for all files

Files	Import difference
There are 4707 files with changed transitive imports taking up over 192447 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

Mathlib/Init.lean

grunweg · 2024-08-15T20:12:08Z

I pushed a commit fixing almost all tests. tests/MinImports.lean needs more careful thought. @adomani Do you have a moment to take a look?

grunweg · 2024-08-15T20:14:55Z

!bench

adomani · 2024-08-15T20:34:30Z

I'm not at a computer, but is the error just some whitespace noise? I'm only going by what I can see in the CI report, though.

leanprover-bot · 2024-08-15T20:37:24Z

Here are the benchmark results for commit 3f6f538.
There were no significant changes against commit 5b6785c.

adomani · 2024-08-15T22:09:16Z

Michael, thank you very much for using the file already!

I took the liberty of fixing the failing MinImports test and, while I was at it, I also reduced the imports in the remaining linters.

I think that all transitive imports are acceptable now, but let's see what the others think about it!

adomani · 2024-08-15T22:33:22Z

By the way, I am not completely sure about what changed with MinImports, but it is something that I had observed before. I think that there are two paths to make the syntax typecheck and Lean genuinely uses one or the other depending on what is available. I do not know why Lean now prefers the "shorter" path, but I would not worry about it too much.

adomani · 2024-08-16T04:38:41Z

Oops, I merged master by mistake, sorry!

By the way, I think that back-porting all the linting changes would be welcome!

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

grunweg · 2024-08-16T08:52:54Z

Thanks for quickly fixing the test, and tweaking the linters. I just filed #15868 and (edit: changed) #15872 for backporting the linter fixes.

grunweg · 2024-08-16T09:13:41Z

I have added a comment inlining Mathlib.Tactic.Linter: it only contained a single import now, and was only meaningfully imported in Mathlib.Tactic.Common. (And, to be honest, I'm not convinced importing it in Tactic.Basic is not a better choice... but that's for another thread.)

Fix long lines, remove unused tactics and add missing end. The remaining changes are silencing linters, which cannot be backported. Split out from #15845.

grunweg · 2024-08-28T12:00:01Z

CI passes now 🎉

kim-em · 2024-08-29T02:11:51Z

bors merge

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file. Hence, move them to `Mathlib.Init`, which has precisely this purpose. All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default. Linters missing from this list include - Linter/Textbased (which is not syntax-based) - Linter/MinImports (which is off by default) - Linter/HaveLet (which is disabled right now) All linters only have imports in `Lean`, except for `Linter/Lint` (which imports `Batteries.Tactic.Lint` to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early. Co-authored-by: adomani <adomani@gmail.com>

mathlib-bors · 2024-08-29T03:10:35Z

Build failed:

Build

bryangingechen · 2024-08-29T06:45:06Z

Looks like it needs another merge with master
bors d+

mathlib-bors · 2024-08-29T06:45:09Z

✌️ 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.

test/fail_if_no_progress.lean

grunweg · 2024-08-29T15:12:01Z

All CI steps pass (except linting, which passed in the previous commit). Thanks for the review!
bors merge

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file. Hence, move them to `Mathlib.Init`, which has precisely this purpose. All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default. Linters missing from this list include - Linter/Textbased (which is not syntax-based) - Linter/MinImports (which is off by default) - Linter/HaveLet (which is disabled right now) All linters only have imports in `Lean`, except for `Linter/Lint` (which imports `Batteries.Tactic.Lint` to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early. Co-authored-by: adomani <adomani@gmail.com>

mathlib-bors · 2024-08-29T16:16:21Z

Pull request successfully merged into master.

Build succeeded:

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

Fix long lines, remove unused tactics and add missing end commands. The remaining changes are silencing linters in `tests`, which cannot be backported. Split out from #15845.

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file. Hence, move them to `Mathlib.Init`, which has precisely this purpose. All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default. Linters missing from this list include - Linter/Textbased (which is not syntax-based) - Linter/MinImports (which is off by default) - Linter/HaveLet (which is disabled right now) All linters only have imports in `Lean`, except for `Linter/Lint` (which imports `Batteries.Tactic.Lint` to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early. Co-authored-by: adomani <adomani@gmail.com>

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

Fix long lines, remove unused tactics and add missing end commands. The remaining changes are silencing linters in `tests`, which cannot be backported. Split out from #15845.

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file. Hence, move them to `Mathlib.Init`, which has precisely this purpose. All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default. Linters missing from this list include - Linter/Textbased (which is not syntax-based) - Linter/MinImports (which is off by default) - Linter/HaveLet (which is disabled right now) All linters only have imports in `Lean`, except for `Linter/Lint` (which imports `Batteries.Tactic.Lint` to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early. Co-authored-by: adomani <adomani@gmail.com>

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

Fix long lines, remove unused tactics and add missing end commands. The remaining changes are silencing linters in `tests`, which cannot be backported. Split out from #15845.

These linters are meant to run on all of mathlib, but they need to be imported in order to run on a given file. Hence, move them to `Mathlib.Init`, which has precisely this purpose. All linters moved in this PR are syntax linters (which need to be imported to run) which are enabled by default. Linters missing from this list include - Linter/Textbased (which is not syntax-based) - Linter/MinImports (which is off by default) - Linter/HaveLet (which is disabled right now) All linters only have imports in `Lean`, except for `Linter/Lint` (which imports `Batteries.Tactic.Lint` to define an environment linter). This import could be avoided by splitting the environment linters into a different file; there is no need to import these syntax linters this early. Co-authored-by: adomani <adomani@gmail.com>

grunweg added RFC Request for comment t-linter Linter labels Aug 15, 2024

grunweg changed the title ~~Mr move linters up~~ RFC/chore: import enabled mathlib syntax linters in Mathlib.Init Aug 15, 2024

ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 15, 2024

adomani reviewed Aug 15, 2024

View reviewed changes

Mathlib/Init.lean Outdated Show resolved Hide resolved

adomani reviewed Aug 15, 2024

View reviewed changes

Mathlib/Init.lean Outdated Show resolved Hide resolved

adomani reviewed Aug 15, 2024

View reviewed changes

Mathlib/Init.lean Outdated Show resolved Hide resolved

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 15, 2024

grunweg force-pushed the MR-move-linters-up branch from e047aa9 to 4533aff Compare August 15, 2024 18:28

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 Aug 15, 2024

grunweg force-pushed the MR-move-linters-up branch from 4533aff to ee33037 Compare August 15, 2024 19:03

grunweg force-pushed the MR-move-linters-up branch from ceb84d4 to 9df35cf Compare August 16, 2024 08:44

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

chore: add missing end

1bc32e9

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

grunweg mentioned this pull request Aug 16, 2024

[Merged by Bors] - chore: add missing end #15868

Closed

grunweg force-pushed the MR-move-linters-up branch from 9df35cf to d8a7d6c Compare August 16, 2024 08:51

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 16, 2024

grunweg mentioned this pull request Aug 16, 2024

chore: fix remaining linters in mathlib and tests #15869

Closed

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

chore(tests): fix linter warnings

f95bdf0

Fix long lines, remove unused tactics and add missing end. The remaining changes are silencing linters, which cannot be backported. Split out from #15845.

grunweg mentioned this pull request Aug 16, 2024

[Merged by Bors] - chore(tests): fix linter warnings #15872

Closed

Silence noisy test

8fbd568

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 28, 2024

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

bryangingechen removed the ready-to-merge This PR has been sent to bors. label Aug 29, 2024

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 29, 2024

grunweg added 2 commits August 29, 2024 15:44

Merge branch 'master' into MR-move-linters-up

9ba564b

Adjust tests for the setOption rename.

edef4ca

grunweg commented Aug 29, 2024

View reviewed changes

test/fail_if_no_progress.lean Outdated Show resolved Hide resolved

Update test/fail_if_no_progress.lean

7fb2b66

mathlib-bors bot changed the title ~~chore: import enabled mathlib syntax linters in Mathlib.Init~~ [Merged by Bors] - chore: import enabled mathlib syntax linters in Mathlib.Init Aug 29, 2024

mathlib-bors bot closed this Aug 29, 2024

mathlib-bors bot deleted the MR-move-linters-up branch August 29, 2024 16:16

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore: add missing end (#15868)

2a96400

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore: add missing end (#15868)

2434e93

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024

chore: add missing end (#15868)

1c24613

Fix mathlib for running the missingEnd linter everywhere. Prerequiste to #15845.

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 7fb2b66537

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Aug 15, 2024

Uh oh!

grunweg commented Aug 15, 2024

Uh oh!

adomani commented Aug 15, 2024

Uh oh!

leanprover-bot commented Aug 15, 2024

Uh oh!

adomani commented Aug 15, 2024

Uh oh!

adomani commented Aug 15, 2024

Uh oh!

adomani commented Aug 16, 2024

Uh oh!

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

Uh oh!

Uh oh!

grunweg commented Aug 16, 2024

Uh oh!

grunweg commented Aug 28, 2024

Uh oh!

kim-em commented Aug 29, 2024

Uh oh!

mathlib-bors bot commented Aug 29, 2024

Uh oh!

bryangingechen commented Aug 29, 2024

Uh oh!

mathlib-bors bot commented Aug 29, 2024

Uh oh!

Uh oh!

grunweg commented Aug 29, 2024

Uh oh!

mathlib-bors bot commented Aug 29, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

grunweg commented Aug 15, 2024 •

edited

Loading

github-actions bot commented Aug 15, 2024 •

edited

Loading

grunweg commented Aug 16, 2024 •

edited

Loading