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

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

Closed
wants to merge 25 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented May 26, 2024

This is one in a series of PRs rewriting most checks from lint-style.py in Lean.
This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247.

This PR also adds a nolints file for text-based linters.


This linter is slightly slower than the Python linter: in local testing,

  • I believe the Python linter took about 0.6s
  • running just lake exe lint_style with a no-op linter (incrementing a counter on each file) takes 0.4s
    (time lake exe lint_style reports real 0m0,404s; user 0m0,254s; sys 0m0,070s; this is the second time when no re-compilation is needed)
  • with the copyright linter, it takes 0.8s
    Any insight into minimising the no-op overhead is welcome (but almost surely out of scope for this PR).

@grunweg grunweg added awaiting-review t-linter Linter tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels May 26, 2024
@grunweg grunweg force-pushed the MR-rewrite-copyright-linter branch from b32817e to bb0d550 Compare May 27, 2024 07:46
@grunweg grunweg force-pushed the MR-rewrite-copyright-linter branch from e09bf3b to 570fb91 Compare May 27, 2024 08:26
scripts/lint-style.sh Outdated Show resolved Hide resolved
@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 Jun 10, 2024
Copy link

github-actions bot commented Jun 10, 2024

PR summary 18dae01c0b

Import changes

No significant changes to the import graph


Declarations diff

+ allLinters
+ copyrightHeaderLinter
+ isCorrectAuthorsLine

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>

@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 Jun 10, 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 Jun 19, 2024
@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 Jun 21, 2024
@grunweg grunweg force-pushed the MR-rewrite-copyright-linter branch from deb385c to 4aab587 Compare June 21, 2024 11:31
@grunweg grunweg force-pushed the MR-rewrite-copyright-linter branch from 4aab587 to 9b16f4e Compare June 21, 2024 11:33
@kim-em
Copy link
Contributor

kim-em commented Jun 23, 2024

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 23, 2024
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 23, 2024

Merge conflict.

@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 Jun 23, 2024
@kim-em kim-em removed the ready-to-merge This PR has been sent to bors. label Jun 23, 2024
@kim-em
Copy link
Contributor

kim-em commented Jun 23, 2024

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 23, 2024

✌️ 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 grunweg force-pushed the MR-rewrite-copyright-linter branch from 9d5bfa2 to 18dae01 Compare June 23, 2024 12:39
@grunweg 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 23, 2024
@grunweg
Copy link
Collaborator Author

grunweg commented Jun 23, 2024

Thanks for the review! Since CI passes now, let me bors it already:
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2024
This is one in a series of PRs rewriting most checks from `lint-style.py` in Lean.
This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247.

This PR also adds a `nolints` file for text-based linters.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: rewrite the copyright header check in Lean [Merged by Bors] - feat: rewrite the copyright header check in Lean Jun 23, 2024
@mathlib-bors mathlib-bors bot closed this Jun 23, 2024
@mathlib-bors mathlib-bors bot deleted the MR-rewrite-copyright-linter branch June 23, 2024 12:53
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
This is one in a series of PRs rewriting most checks from `lint-style.py` in Lean.
This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247.

This PR also adds a `nolints` file for text-based linters.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
This is one in a series of PRs rewriting most checks from `lint-style.py` in Lean.
This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247.

This PR also adds a `nolints` file for text-based linters.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated t-linter Linter tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants