[Merged by Bors] - chore: a non-lean linter for #-commands #10809
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
adomani
added
awaiting-review
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 22, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
|
Okay, not lovely, but better than nothing! :-) bors d+ |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
Thanks for the approval and for merging the remaining "test" PR. I hope that this is just a temporary fix. I'm trying to see how actual Lean linters work and hopefully I'll be able to replace this one by a proper linter. |
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 22, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
thorimur
pushed a commit
that referenced
this pull request
Feb 24, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
thorimur
pushed a commit
that referenced
this pull request
Feb 24, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
|
I think this would have been better to add as an extra linter for the style linter python script. In the same way as we ban set option there. This would be a much less complicated way of doing things imo, and we would get things like reviewdog for free almost |
thorimur
pushed a commit
that referenced
this pull request
Feb 26, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
thorimur
pushed a commit
that referenced
this pull request
Feb 26, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
adomani
added a commit
that referenced
this pull request
Feb 27, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
|
@alexjbest in case you are curious, I have a draft version of the same linter, but written in lean as a "syntax linter": #11019. If that one is preferred, then I am happy to remove this one! |
riccardobrasca
pushed a commit
that referenced
this pull request
Mar 1, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
riccardobrasca
pushed a commit
that referenced
this pull request
Mar 1, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
Louddy
pushed a commit
that referenced
this pull request
Apr 15, 2024
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
Louddy
pushed a commit
that referenced
this pull request
Apr 15, 2024
This PR introduces an `awk`-based linter for checking that `Mathlib/*.lean` files do not contain `#`-commands. It takes the names of the commands that begin with `#` by running ```lean import Mathlib #help command ``` and after that it is all text-based substitutions. It triggers an error on lines that begin with `#cmd`, omitting (most) lines contained comment blocks. CI for this PR should fail until #10772 and #10827 have been merged.
1 task
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 24, 2024
A Lean-linter implementation of the `#`-command linter introduced in #10809. This linter produces a warning whenever a non-allowed `#`-command is used. The allowed commands are ```lean #align #align_import #noalign #adaptation_note ``` [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311019.3A.20a.20syntax.20linter.20for.20.23-commands) Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
grunweg
added a commit
that referenced
this pull request
May 24, 2024
A Lean-linter implementation of the `#`-command linter introduced in #10809. This linter produces a warning whenever a non-allowed `#`-command is used. The allowed commands are ```lean #align #align_import #noalign #adaptation_note ``` [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311019.3A.20a.20syntax.20linter.20for.20.23-commands) Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces an
awk-based linter for checking thatMathlib/*.leanfiles do not contain#-commands.It takes the names of the commands that begin with
#by runningand after that it is all text-based substitutions.
It triggers an error on lines that begin with
#cmd, omitting (most) lines contained comment blocks.CI for this PR should fail until #10772 and #10827 have been merged.
#10772 has been merged and the error message for the check decreased.
#10827 has been merged and the error message disappeared.