[Merged by Bors] - feat: `dupNamespace` as a syntax linter #11154

adomani · 2024-03-04T18:06:40Z

An implementation of the dupNamespace from Std as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace:

Nat.Nat.foo triggers the linter;
Nat.foo.Nat does not trigger the linter.

Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

Zulip discussion

The linter found

private theorem Seminorm.Seminorm.isLUB_sSup ...

that is skipped by the environment dupNamespace linter.

A note on the extra import: it is only used to get Array.attach, which allows to write

def getIds : Syntax → Array Syntax
  | stx@(.node _ _ args) =>
    ((args.attach.map fun ⟨a, _⟩ => getIds a).foldl (· ++ ·) #[stx]).filter (·.getKind == ``declId)
  | _ => default

and not have to mark it as partial.

…11161) A private duplicated namespace found by the linter in #11154.

alexjbest · 2024-03-05T14:38:55Z

!bench

leanprover-bot · 2024-03-05T15:17:05Z

Here are the benchmark results for commit de74382.
There were no significant changes against commit 39f3b00.

…11161) A private duplicated namespace found by the linter in #11154.

YaelDillies

maintainer merge

Mathlib/Tactic/Lint.lean

github-actions · 2024-03-26T13:15:12Z

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

github-actions · 2024-03-26T13:15:13Z

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

…e_syntax

test/Simps.lean

mattrobball · 2024-03-28T14:21:11Z

It would be nice to have tests for the behavior under exporting and aliasing also.

adomani · 2024-03-28T18:32:27Z

!bench

adomani · 2024-03-28T18:35:13Z

I added checking for alias: it was slightly awkward, since the "name" node for alias is ident, while the one for theorem/lemma is declId. I have not checked what happens with export, though.

adomani · 2024-03-28T19:15:54Z

Here are the benchmark results for commit 9c29121. The entire run failed. Found no significant differences.

The bench ~~should happen~~ at #11747 reported no significant changes.

mattrobball · 2024-03-28T22:16:12Z

Great!

Can you write a test for naming via export and comment it out with some explanation if it doesn't work?

bors delegate+

mathlib-bors · 2024-03-28T22:16: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.

adomani · 2024-03-28T22:52:47Z

Matt, thanks! I added support for export and a test. Assuming that CI is happy with the change, I will merge!

adomani · 2024-03-29T04:50:00Z

bors r+

An implementation of the `dupNamespace` from `Std` as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace: * `Nat.Nat.foo` triggers the linter; * `Nat.foo.Nat` does *not* trigger the linter. *Note.* This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose `declId` is present in the source declaration). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60dupNamespace.60.20linter) The linter found ```lean private theorem Seminorm.Seminorm.isLUB_sSup ... ``` that is skipped by the environment `dupNamespace` linter.

mathlib-bors · 2024-03-29T06:00:06Z

Pull request successfully merged into master.

Build succeeded:

…11161) A private duplicated namespace found by the linter in #11154.

An implementation of the `dupNamespace` from `Std` as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace: * `Nat.Nat.foo` triggers the linter; * `Nat.foo.Nat` does *not* trigger the linter. *Note.* This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose `declId` is present in the source declaration). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60dupNamespace.60.20linter) The linter found ```lean private theorem Seminorm.Seminorm.isLUB_sSup ... ``` that is skipped by the environment `dupNamespace` linter.

…11161) A private duplicated namespace found by the linter in #11154.

An implementation of the `dupNamespace` from `Std` as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace: * `Nat.Nat.foo` triggers the linter; * `Nat.foo.Nat` does *not* trigger the linter. *Note.* This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose `declId` is present in the source declaration). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60dupNamespace.60.20linter) The linter found ```lean private theorem Seminorm.Seminorm.isLUB_sSup ... ``` that is skipped by the environment `dupNamespace` linter.

adomani added 7 commits March 4, 2024 18:04

feat: dupNamespace as a syntax linter

8877b8b

Whitespace and open

6dea1f7

Add docs

fcea966

Maybe fix?

7420041

Remove duplicate namespace!

9b5f2a7

Print full name

9d96fe8

unlint a test file

0402dd7

adomani added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Mar 4, 2024

adomani added 4 commits March 4, 2024 22:53

Reduce imports, use private declaration

2dd5807

Add warning about autogenerated declarations

b3bea3f

Remove partial, increase imports

8868369

Add dupNamespace tests

a4244db

adomani mentioned this pull request Mar 4, 2024

[Merged by Bors] - chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup #11161

Closed

adomani added 2 commits March 5, 2024 00:06

Avoid panic in tail!

b9f43fd

Omit isBlackListed: the linter only sees syntax

de74382

mathlib-bors bot pushed a commit that referenced this pull request Mar 5, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

13df034

…11161) A private duplicated namespace found by the linter in #11154.

mathlib-bors bot pushed a commit that referenced this pull request Mar 5, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

8c06311

…11161) A private duplicated namespace found by the linter in #11154.

adomani added 3 commits March 5, 2024 16:54

Merge branch 'master' into adomani/dupNamespace_syntax

0e341d4

Remove non-existent import

47f657f

Remove imports in tests

4c03ff3

kbuzzard pushed a commit that referenced this pull request Mar 12, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

ff291cb

…11161) A private duplicated namespace found by the linter in #11154.

dagurtomas pushed a commit that referenced this pull request Mar 22, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

679cb6c

…11161) A private duplicated namespace found by the linter in #11154.

utensil pushed a commit that referenced this pull request Mar 26, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

23d5ca8

…11161) A private duplicated namespace found by the linter in #11154.

YaelDillies approved these changes Mar 26, 2024

View reviewed changes

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

github-actions bot added the maintainer-merge label Mar 26, 2024

adomani added 2 commits March 26, 2024 20:36

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

8b14fdf

…e_syntax

logLint, instead of logWarning

b7e0a85

mattrobball reviewed Mar 28, 2024

View reviewed changes

test/Simps.lean Outdated Show resolved Hide resolved

adomani added 2 commits March 28, 2024 17:58

Merge branch 'master' into adomani/dupNamespace_syntax

e1ea4a1

Please the linter by renaming, instead of setting options

c3d91e7

Lint also alias

a778c08

adomani force-pushed the adomani/dupNamespace_syntax branch from 9c29121 to a778c08 Compare March 28, 2024 18:33

This comment was marked as resolved.

Sign in to view

test also alias

0ec2ec3

adomani mentioned this pull request Mar 28, 2024

test dupNamespace speed #11747

Closed

Add export

017c450

mathlib-bors bot changed the title ~~feat: dupNamespace as a syntax linter~~ [Merged by Bors] - feat: dupNamespace as a syntax linter Mar 29, 2024

mathlib-bors bot closed this Mar 29, 2024

mathlib-bors bot deleted the adomani/dupNamespace_syntax branch March 29, 2024 06:00

Louddy pushed a commit that referenced this pull request Apr 15, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

3ea70d1

…11161) A private duplicated namespace found by the linter in #11154.

callesonne pushed a commit that referenced this pull request Apr 22, 2024

chore: Remove duplicate namespace in Seminorm.Seminorm.isLUB_sSup (#…

4eecccb

…11161) A private duplicated namespace found by the linter in #11154.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: `dupNamespace` as a syntax linter #11154

[Merged by Bors] - feat: `dupNamespace` as a syntax linter #11154

adomani commented Mar 4, 2024 •

edited

alexjbest commented Mar 5, 2024

leanprover-bot commented Mar 5, 2024

YaelDillies left a comment

github-actions bot commented Mar 26, 2024

github-actions bot commented Mar 26, 2024

mattrobball commented Mar 28, 2024

adomani commented Mar 28, 2024

adomani commented Mar 28, 2024

This comment was marked as resolved.

adomani commented Mar 28, 2024 •

edited

mattrobball commented Mar 28, 2024

mathlib-bors bot commented Mar 28, 2024

adomani commented Mar 28, 2024

adomani commented Mar 29, 2024

mathlib-bors bot commented Mar 29, 2024

[Merged by Bors] - feat: dupNamespace as a syntax linter #11154

[Merged by Bors] - feat: dupNamespace as a syntax linter #11154

Conversation

adomani commented Mar 4, 2024 • edited

alexjbest commented Mar 5, 2024

leanprover-bot commented Mar 5, 2024

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented Mar 26, 2024

github-actions bot commented Mar 26, 2024

mattrobball commented Mar 28, 2024

adomani commented Mar 28, 2024

adomani commented Mar 28, 2024

This comment was marked as resolved.

adomani commented Mar 28, 2024 • edited

mattrobball commented Mar 28, 2024

mathlib-bors bot commented Mar 28, 2024

adomani commented Mar 28, 2024

adomani commented Mar 29, 2024

mathlib-bors bot commented Mar 29, 2024

[Merged by Bors] - feat: `dupNamespace` as a syntax linter #11154

[Merged by Bors] - feat: `dupNamespace` as a syntax linter #11154

adomani commented Mar 4, 2024 •

edited

adomani commented Mar 28, 2024 •

edited