Skip to content

[Merged by Bors] - chore: a non-lean linter for #-commands#10809

Closed
adomani wants to merge 9 commits intomasterfrom
adomani/hash_commands
Closed

[Merged by Bors] - chore: a non-lean linter for #-commands#10809
adomani wants to merge 9 commits intomasterfrom
adomani/hash_commands

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented Feb 21, 2024 •
edited
Loading

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

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.

#10772 has been merged and the error message for the check decreased.

#10827 has been merged and the error message disappeared.

Open in Gitpod

@adomani adomani added awaiting-review CI Modifies the continuous integration setup or other automation labels Feb 21, 2024
@adomani adomani mentioned this pull request Feb 21, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Feb 22, 2024
@adomani
chore: move #guard_msgs in PosDef to test file (#10827)
096b9e1 
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Feb 22, 2024

Okay, not lovely, but better than nothing! :-)

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 22, 2024

✌️ 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.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 22, 2024
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 22, 2024

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.

@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 22, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 22, 2024
@adomani
chore: a non-lean linter for #-commands (#10809)
7289300 
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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 22, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: a non-lean linter for #-commands [Merged by Bors] - chore: a non-lean linter for #-commands Feb 22, 2024
@mathlib-bors mathlib-bors bot closed this Feb 22, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/hash_commands branch February 22, 2024 04:38
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@adomani @thorimur
chore: move #guard_msgs in PosDef to test file (#10827)
872440e 
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
@adomani @thorimur
chore: a non-lean linter for #-commands (#10809)
0b1f76f 
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.
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Feb 25, 2024

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
@adomani @thorimur
chore: move #guard_msgs in PosDef to test file (#10827)
ff52e97 
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
@adomani @thorimur
chore: a non-lean linter for #-commands (#10809)
1e13059 
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
@adomani
chore: move #guard_msgs in PosDef to test file (#10827)
634caec 
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
@adomani adomani mentioned this pull request Feb 27, 2024
Closed
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Feb 27, 2024

@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
@adomani @riccardobrasca
chore: move #guard_msgs in PosDef to test file (#10827)
d1a6a73 
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
@adomani @riccardobrasca
chore: a non-lean linter for #-commands (#10809)
d75e138 
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
@adomani @dagurtomas
chore: move #guard_msgs in PosDef to test file (#10827)
dd3d7ed 
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
@adomani @dagurtomas
chore: a non-lean linter for #-commands (#10809)
a45489d 
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.
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@adomani @xgenereux
chore: move #guard_msgs in PosDef to test file (#10827)
8e8fca7 
This PR moves a `#guard_msgs` command from `LinearAlgebra/Matrix/PosDef` to a test file: it is a preparation for #10809.
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@adomani @xgenereux
chore: a non-lean linter for #-commands (#10809)
9a0f951 
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.
@grunweg grunweg mentioned this pull request May 5, 2024
Closed
1 task
mathlib-bors bot pushed a commit that referenced this pull request May 24, 2024
@adomani @grunweg
feat: syntax linter for #-commands (#11019)
f966474 
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
@adomani @grunweg
feat: syntax linter for #-commands (#11019)
79969aa 
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>
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@adomani @grunweg @callesonne
feat: syntax linter for #-commands (#11019)
0e249c5 
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>
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@adomani @grunweg @js2357
feat: syntax linter for #-commands (#11019)
a3d188c 
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

Reviewers

No reviews

Assignees

No one assigned

Labels

CI Modifies the continuous integration setup or other automation delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@adomani @kim-em @alexjbest