Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: generic linter, absorbing cdot linter and attribute [instance] in linter #12143

Open
wants to merge 21 commits into
base: master
Choose a base branch
from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 15, 2024

A "generic" syntax linter that can be configured using a function Syntax → Array Syntax.
The expectations is that the function returns sub-syntax extracted from the input that should be flagged by the linter.

This PR provides two examples.


Open in Gitpod

@adomani
Copy link
Collaborator Author

adomani commented Apr 15, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit b9ee1c4.
There were no significant changes against commit 7c5b29b.

mathlib-bors bot pushed a commit that referenced this pull request Apr 15, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
Louddy pushed a commit that referenced this pull request Apr 15, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 24, 2024
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
A simple replacement `. --> ·`.

See #12143 for the source of these replacements.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 10, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2024
Replace two `.` with `·`.

Found by the linter at #12143.
apnelson1 pushed a commit that referenced this pull request May 12, 2024
Replace two `.` with `·`.

Found by the linter at #12143.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2024
callesonne pushed a commit that referenced this pull request May 16, 2024
Replace two `.` with `·`.

Found by the linter at #12143.
grunweg pushed a commit that referenced this pull request May 17, 2024
Replace two `.` with `·`.

Found by the linter at #12143.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 20, 2024
@grunweg
Copy link
Collaborator

grunweg commented May 23, 2024

awaiting-author

@github-actions github-actions bot added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 23, 2024
@adomani adomani added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 25, 2024
@adomani
Copy link
Collaborator Author

adomani commented May 25, 2024

Michael, thanks for reviewing!

I had intended this PR as an experiment for the "generic" framework and I thought that cdot was a good candidate, since it is just a style lint, rather than something more substantial.

However, as a further experiment, you can see how now the linter is flexible enough to lint against both cdots and your "attribute_instance_in" uniformly.

@adomani adomani changed the title feat: a cdot linter feat: generic linter, absorbing cdot linter and attribute [instance] in linter May 25, 2024
@grunweg
Copy link
Collaborator

grunweg commented May 25, 2024

🎉 Wow, thanks for rewriting my linter!
I wasn't sure whether an attribute declaration was always at the top (as opposed to possibly being nested): it seems it always is, so your simplification works. And I like your test file - it's both slightly more comprehensive and requires fewer imports than what I cobbled together.

I see some tension between code duplication and error messages: having all errors be about linter.generic is a strictly worse user experience; deduplicating the same boilerplate is also annoying.

@adomani
Copy link
Collaborator Author

adomani commented May 25, 2024

Maybe we could have something like set_option no_lint "cdot" to selectively disable cdot. I think that Strings can be supported.

The implementation of the linter would need to handle these refined options.

Also, we may have to disengage from logLint.

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 25, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 26, 2024
Copy link

github-actions bot commented Jul 22, 2024

PR summary bb394346c8

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
There are 4003 files with changed transitive imports: this is too many to display!

Declarations diff

+ findDot
+ genericSyntaxLinter
+ getLinterHash
+ instance : Inhabited Nat
+ isCDot?
+ is_attribute_instance_in
+ unwanted.cDot
+++++++++++++ instance : Inhabited Int

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>

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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 22, 2024
@riccardobrasca riccardobrasca removed the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 23, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-linter Linter
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants