[Merged by Bors] - feat: add `endOf` linter by adomani · Pull Request #14378 · leanprover-community/mathlib4

adomani · 2024-07-03T06:59:21Z

This linter emits a warning at the end of a file if there are unclosed namespaces or sections.
All missing ends have been added (automatically) in #14621.

Unlike #14352, this PR does leaves outermost noncomputable sections open.

Zulip thread

Self-correcting script:

eval "$(
  lake build |
    grep -v "^\(✔ \[\|note: \|⚠ \[\|trace: \|Build completed\)" |
      sed -z "s=warning: \./\./\./\./\([^:]*\):[^']*'\([^']*\)'\n=\nprintf '\2\\n' >> \1\n\n\n=g" |
      sed -z "s=\n\n*=\n=g; s=\([^']\)\nend=\1\n\nend=g"
)"

github-actions · 2024-07-03T07:00:00Z

PR summary b600a781ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ endOfLinter
+ getLinterHash

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>

…_allow_noncomputable

grunweg

Thanks for writing this linter! Looks very nice overall --- I have some suggestions for polish, code clarity etc.
I pushed those directly: if you disagree with any or have further suggestions, I'm very interested in your opinion. Notably, I have tweaked the linter error message; your script will need adaptation.

I have not reviewed the automatic fixes yet, will do so next.

What do you think about adding a test?
I'm not sold on the name "EndOf" yet: what do you think about "openSectionsNamespaces", "unclosedSectionsNamespaces" or perhaps "unclosedScopes"?

grunweg

I've gone through all the automatic changes now. Obviously, they are all correct (in the sense that they compile and pass the linter). A few times, they expose pre-existing weirdness; I'd prefer to fix that instead. (This could be a pre-requisite PR which I can approve quickly.)

Mathlib/Algebra/Category/ModuleCat/Sheaf/Colimits.lean

grunweg · 2024-07-10T15:52:39Z

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

    · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩
+
+end induced_subgraphs


Pre-existing: do we have a policy that section names should be CamelCase or match their declarations?

Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

Mathlib/Probability/Distributions/Uniform.lean

Mathlib/RingTheory/Bialgebra/Basic.lean

grunweg · 2024-07-10T16:04:56Z

Mathlib/Tactic/Positivity/Basic.lean

+
+end Positivity
+
+end Meta


Also pre-existing: tactics are sometimes in the Meta and sometimes in the Tactic namespaces: is there an intentional difference? (Presumably also out of scope of this PR.)

Mathlib/Topology/ExtremallyDisconnected.lean

Mathlib/Topology/Separation.lean

test/Lint.lean

grunweg · 2024-07-10T16:09:00Z

test/Traversable.lean


 end
+
+end Testing


This namespace is inconsistent with the other tests -> rename to Tests instead?

grunweg · 2024-07-10T16:15:02Z

#14620 contains a few of these fixes.
As discussed with adomani, let's land these fixes as a follow-up, and land the linter now.

Mathlib/Tactic/Linter/Lint.lean

grunweg · 2024-07-10T22:02:24Z

The fixes to the other files have landed; I have merged master. This PR now just contains the linter.
I still think the implementation is good.
maintainer merge

github-actions · 2024-07-10T22:02:34Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

jcommelin

Thanks 🎉

bors merge

This linter emits a warning at the end of a file if there are unclosed `namespace`s or `section`s. All missing `end`s have been added (automatically) in #14621. Unlike #14352, this PR does leaves outermost `noncomputable section`s open. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20for.20unclosed.20sections.3F) Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de> Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

mathlib-bors · 2024-07-11T13:27:08Z

Build failed (retrying...):

Build

This linter emits a warning at the end of a file if there are unclosed `namespace`s or `section`s. All missing `end`s have been added (automatically) in #14621. Unlike #14352, this PR does leaves outermost `noncomputable section`s open. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20for.20unclosed.20sections.3F) Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de> Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

mathlib-bors · 2024-07-11T14:01:58Z

Build failed (retrying...):

Build

mattrobball · 2024-07-11T14:13:17Z

bors r-

mathlib-bors · 2024-07-11T14:13:19Z

Canceled.

mattrobball · 2024-07-11T14:13:33Z

Wronskian violates the linter and just got in

mattrobball · 2024-07-11T14:15:12Z

bors delegate+

Please merge again when fixed

mathlib-bors · 2024-07-11T14:15:14Z

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

…_allow_noncomputable

adomani · 2024-07-11T14:59:12Z

bors r+

This linter emits a warning at the end of a file if there are unclosed `namespace`s or `section`s. All missing `end`s have been added (automatically) in #14621. Unlike #14352, this PR does leaves outermost `noncomputable section`s open. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20for.20unclosed.20sections.3F) Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de> Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

mathlib-bors · 2024-07-11T15:08:59Z

Pull request successfully merged into master.

Build succeeded:

feat: add endOf linter

e030e35

add ends

5fb2857

adomani mentioned this pull request Jul 3, 2024

feat: the endOf linter #14352

Closed

adomani added 2 commits July 3, 2024 10:30

Archive

8cfa334

tests

fa93594

adomani added awaiting-review t-linter Linter labels Jul 3, 2024

adomani added 3 commits July 3, 2024 18:59

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

20b4c27

…_allow_noncomputable

one more end

33d2261

end end

d2a3706

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 Jul 5, 2024

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

fe701b4

…_allow_noncomputable

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

adomani added 4 commits July 6, 2024 19:01

fixes

7606a8b

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

0c71c30

…_allow_noncomputable

add end ZMod

ccc4746

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

4ff9ae9

…_allow_noncomputable

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 Jul 8, 2024

kim-em removed the awaiting-review label Jul 9, 2024

adomani added 2 commits July 10, 2024 15:45

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

8772a4d

…_allow_noncomputable

add more ends

b5a1082

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

adomani and others added 3 commits July 10, 2024 16:58

more fixes

59ed1a6

Remove duplicate namespace; stylistic tweaks.

649a81a

Tweak documentation and error message.

fa5693f

grunweg reviewed Jul 10, 2024

View reviewed changes

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

ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is 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 Jul 10, 2024

Merge branch 'master' into adomani/endOfLinter_allow_noncomputable

28832fb

grunweg removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 10, 2024

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 10, 2024

grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 10, 2024

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

jcommelin reviewed Jul 11, 2024

View reviewed changes

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

adomani added 2 commits July 11, 2024 16:37

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

a1ec7ac

…_allow_noncomputable

end polynomial

b600a78

mathlib-bors bot changed the title ~~feat: add endOf linter~~ [Merged by Bors] - feat: add endOf linter Jul 11, 2024

mathlib-bors bot closed this Jul 11, 2024

mathlib-bors bot deleted the adomani/endOfLinter_allow_noncomputable branch July 11, 2024 15:09

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

adomani commented Jul 3, 2024 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary b600a781ce

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg Jul 10, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg Jul 10, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg Jul 10, 2024

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jul 10, 2024

Uh oh!

github-actions bot commented Jul 10, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jul 11, 2024

Uh oh!

mathlib-bors bot commented Jul 11, 2024

Uh oh!

mattrobball commented Jul 11, 2024

Uh oh!

mathlib-bors bot commented Jul 11, 2024

Uh oh!

mattrobball commented Jul 11, 2024

Uh oh!

mattrobball commented Jul 11, 2024

Uh oh!

mathlib-bors bot commented Jul 11, 2024

Uh oh!

adomani commented Jul 11, 2024

Uh oh!

mathlib-bors bot commented Jul 11, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

adomani commented Jul 3, 2024 •

edited by grunweg

Loading

github-actions bot commented Jul 3, 2024 •

edited

Loading

grunweg commented Jul 10, 2024 •

edited

Loading