[Merged by Bors] - feat: syntax linter for `#`-commands by adomani · Pull Request #11019 · leanprover-community/mathlib4

adomani · 2024-02-27T18:33:17Z

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

#align
#align_import
#noalign
#adaptation_note

Zulip discussion

~~This PR is accompanied by #11028, which places the linter in Tactic.Basic, to make sure that (most of) Mathlib passes the #-command linter~~.

alexjbest · 2024-02-28T23:36:00Z

Mathlib/Tactic/HashCommandLinter.lean

+For example, `#eval, #guard, #guard_msgs` all trigger a message.
+-/
+register_option linter.hashCommand : Bool := {
+  defValue := true


I don't think this should be enabled by default, but it should be enabled in CI (can do so in this PR). What do you think?

I actually think that I prefer it to be disabled by default outside of CI: if I am using #eval in a file, I expect to want to see the output and not be bugged by the linter! I'll look up how to make sure that CI uses a different default.

Yeah I agree exactly, I think its enoguh to call lean in CI with -Dlinter.hashCommand=true

I am failing to make this work locally:

$ lake build Mathlib.mwe [303/304] Building Mathlib.mwe error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/damiano/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean -Dlinter.hashCommand=true -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/mwe.lean -R ././. -o ./.lake/build/lib/Mathlib/mwe.olean -i ./.lake/build/lib/Mathlib/mwe.ilean -c ./.lake/build/ir/Mathlib/mwe.c error: stderr: invalid -D parameter, unknown configuration option 'linter.hashCommand' error: external command `/home/damiano/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean` exited with code 1

I modified this

weakLeanArgs := if get_config? CI |>.isSome then #["-DwarningAsError=true", "-Dlinter.hashCommand=true"] else #["-Dlinter.hashCommand=true"]

Alex, it seems that it is not an option to make this linter quiet locally, but chatty on CI. I propose to make the linter available with quiet default: hopefully in the future it will be possible to set different defaults globally and then the linter would reach its full potential!

Hmm, it's a hack to work around it now, but: what if we made the defValue := true, yet also checked warningAsError in the linter (and left a very visible note, and even made the description "enables the `#`-command linter as long as `warningAsError` is `true`")? I.e.

def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.hashCommand o && warningAsError.get o

Then it would run in CI (since that uses warningAsError := true) but not locally under normal circumstances.

I guess the question is: in practice, would someone want to turn on this linter locally? Or is it ok if it's only ever run in CI?

(Another option is to keep defValue := false but turn it on whenever warningAsError := true, i.e. using || instead of && above.)

For me, the main use of this linter while working on a PR, would be when a #-command is silent. If I am using a "noisy" #-command, I am probably curious about its output and adding the linter warning would be annoying.

If there were a way of making the linter noisy exactly when the #-command is not, then I would like it always on, I think.

Having it on while editing when there are no messages is a good idea! I do wonder whether it should also be on everywhere during CI for good error messages (as mentioned elsewhere). I guess the logic would be getLinterHash (<- getOptions) && ((<- get).messages.msgs.size == 0 || warningAsError.get (<- getOptions)) in that case. I won't insist on this, though! :)

alexjbest · 2024-02-29T00:55:32Z

I like this much more than the sed version!

thorimur

This review seems bigger than it is. It's basically:

style/documentation
code tweaking/taking care of edge cases
questions about a couple of details

This PR looks very nice! :)

Mathlib/Tactic/HashCommandLinter.lean

…ommunity/mathlib4 into adomani/hash_command_linter

thorimur

Apologies for the delay—very close to looking good to me! :) (Also see comment about withSetOptionIn' which is not organized as part of this review.)

I would like to see if we can run this during CI if possible by hijacking the warningAsError option (only until the underlying issue is fixed, of course)—see comment.

Mathlib/Tactic/HashCommandLinter.lean

Mathlib/Tactic.lean

thorimur · 2024-03-30T02:51:20Z

Mathlib/Tactic/HashCommandLinter.lean

+For example, `#eval, #guard, #guard_msgs` all trigger a message.
+-/
+register_option linter.hashCommand : Bool := {
+  defValue := true


Hmm, it's a hack to work around it now, but: what if we made the defValue := true, yet also checked warningAsError in the linter (and left a very visible note, and even made the description "enables the `#`-command linter as long as `warningAsError` is `true`")? I.e.

def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.hashCommand o && warningAsError.get o

Then it would run in CI (since that uses warningAsError := true) but not locally under normal circumstances.

I guess the question is: in practice, would someone want to turn on this linter locally? Or is it ok if it's only ever run in CI?

(Another option is to keep defValue := false but turn it on whenever warningAsError := true, i.e. using || instead of && above.)

…d_linter

adomani · 2024-03-30T08:57:51Z

Thomas, thank you very much for your comments! The new withSetOptionIn' command works great, thanks! I added it and also put some tests in to ensure that it does what it should!

adomani

Oh, I thought that I had replied to those previous messages, but they got lost in review!

Anyway, I ended up allowing more #guards!

Mathlib/Tactic/HashCommandLinter.lean

adomani · 2024-05-23T09:45:41Z

Ok, after yet another failed test, I decided to make the #guards not allowed, except in test other than test.HashCommandLinter. I hope that this time the tests pass!

grunweg · 2024-05-23T11:17:41Z

Tests pass; I took one last look and pushed a few tiny tweaks. (@adomani Feel free to revert those if you prefer!)
I think this lint is ready to go: performance is good, mathlib passes, no bad test changes or anything that looks questionable. Thank you for your work on this, this one took a while - but I'm glad it lands!
maintainer merge

(A follow-up PR could remove the sed-based linter this replaces. Imho, this doesn't have to happen in this PR.)

github-actions · 2024-05-23T11:17:53Z

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

The linter was rewritten in Lean in #11019.

grunweg · 2024-05-23T11:25:35Z

Filed #13142 for the follow-up.

jcommelin · 2024-05-24T03:23:58Z

Thanks 🎉

bors merge

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>

mathlib-bors · 2024-05-24T04:42:20Z

Pull request successfully merged into master.

Build succeeded:

The linter was rewritten in Lean in #11019.

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>

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

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>

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

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>

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

adomani added 3 commits February 27, 2024 18:21

feat: syntax linter for #-commands

01139ce

Do not lint syntax containing spaces

1b7ca08

import new files

4594438

adomani mentioned this pull request Feb 27, 2024

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

Closed

adomani added 3 commits February 27, 2024 20:04

Remove partial, check only first atom

4bd6a60

Only lint `Mathlib files.

d12b297

Only lint `Mathlib files or the HashLinter test file.

018b00a

adomani mentioned this pull request Feb 27, 2024

feat: #-command linter in Tactic.Basic. #11028

Closed

1 task

adomani added awaiting-review t-meta Tactics, attributes or user commands labels Feb 27, 2024

alexjbest reviewed Feb 28, 2024

View reviewed changes

Set the default value to false

ff38396

thorimur reviewed Mar 2, 2024

View reviewed changes

Remove getAtomStx + some of Thomas' comments

19025e6

This comment was marked as resolved.

Sign in to view

adomani added 2 commits March 3, 2024 10:34

Merge branch 'adomani/hash_command_linter' of github.com:leanprover-c…

add0371

…ommunity/mathlib4 into adomani/hash_command_linter

Remove import

9d9f40d

adomani force-pushed the adomani/hash_command_linter branch from ac6194d to 9d9f40d Compare March 3, 2024 09:48

adomani added 2 commits March 3, 2024 10:51

Remove folder

db19d8c

Remove checking for a space

4eb3c32

jcommelin requested a review from thorimur March 26, 2024 08:58

thorimur reviewed Mar 30, 2024

View reviewed changes

adomani added 5 commits March 30, 2024 09:02

Add Thomas' recusion into in and tests

3aeb10e

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

1074485

…d_linter

Update HashCommandLinter.lean

190db33

Update HashCommandLinter.lean

59174f5

Update HashCommandLinter.lean

2ce18aa

Reorder imports

adad167

more allowed guards

84eff9b

adomani commented May 23, 2024

View reviewed changes

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

Mathlib/Tactic/HashCommandLinter.lean Show resolved Hide resolved

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

exclude tests, do not allow #guards

8699ac8

Small tweaks; feel free to revert if you prefer the old code.

f7039b5

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 23, 2024

grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 23, 2024

grunweg added a commit that referenced this pull request May 23, 2024

chore: remove sed-based hashCommand linter

05bb8ed

The linter was rewritten in Lean in #11019.

grunweg mentioned this pull request May 23, 2024

[Merged by Bors] - chore: remove sed-based hashCommand linter #13142

Closed

1 task

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 23, 2024

grunweg added t-linter Linter and removed t-meta Tactics, attributes or user commands labels May 23, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 24, 2024

mathlib-bors bot changed the title ~~feat: syntax linter for #-commands~~ [Merged by Bors] - feat: syntax linter for #-commands May 24, 2024

mathlib-bors bot closed this May 24, 2024

mathlib-bors bot deleted the adomani/hash_command_linter branch May 24, 2024 04:42

grunweg added a commit that referenced this pull request May 24, 2024

chore: remove sed-based hashCommand linter

2ed2b23

The linter was rewritten in Lean in #11019.

mathlib-bors bot pushed a commit that referenced this pull request May 27, 2024

chore: remove sed-based hashCommand linter (#13142)

5902b54

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

callesonne pushed a commit that referenced this pull request Jun 4, 2024

chore: remove sed-based hashCommand linter (#13142)

8f40972

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

js2357 pushed a commit that referenced this pull request Jun 18, 2024

chore: remove sed-based hashCommand linter (#13142)

2e88456

The linter was rewritten in Lean in #11019. This removes one separate workflow step.

Conversation

adomani commented Feb 27, 2024 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Mar 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alexjbest commented Feb 29, 2024

Uh oh!

thorimur left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

This comment was marked as resolved.

Uh oh!

thorimur left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

thorimur Mar 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

adomani commented Mar 30, 2024

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani commented May 23, 2024

Uh oh!

grunweg commented May 23, 2024

Uh oh!

github-actions bot commented May 23, 2024

Uh oh!

grunweg commented May 23, 2024

Uh oh!

jcommelin commented May 24, 2024

Uh oh!

mathlib-bors bot commented May 24, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

adomani commented Feb 27, 2024 •

edited by grunweg

Loading

thorimur Mar 30, 2024 •

edited

Loading

thorimur left a comment •

edited

Loading

thorimur Mar 30, 2024 •

edited

Loading