fix: now linters in general do not run on #guard_msgs itself
#5644
Conversation
The `#guard_msgs` command runs the command it is attached to as if it were a top-level command. This is because the top-level command elaborator runs linters, and we are interested in capturing linter warnings using `#guard_msgs`. However, the linters will run on `#guard_msgs` itself, leading sometimes to duplicate warnings (like for the unused variable linter). Rather than special-casing `#guard_msgs` in every affected linter, this PR special-cases it in the top-level command elaborator itself. Now linters are only run if the command doesn't contain `#guard_msgs`. This way, the linters are only run on the sub-command that `#guard_msgs` runs. It would probably be best to require that `#guard_msgs` *only* be runnable as a top-level command, since there are ways to suppress linting with the current setup.
github-actions
bot
added
the
toolchain-available
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
| -- Run the linters, unless `#guard_msgs` is present, which is special and runs `elabCommandTopLevel` itself, | ||
| -- so it is a "super-top-level" command. This is the only command that does this, so we just special case it here | ||
| -- rather than engineer a general solution. | ||
| unless (stx.find? (·.isOfKind ``Lean.guardMsgsCmd)).isSome do |
There was a problem hiding this comment.
This means that linting for #guard_msgs or "ins that precede it" will become trickier, right?
E.g. the linters would only see section in
variable (x : Nat) in
open Lean in
#guard_msgs in
section?
And something like
open Lean in
run_cmd
let stx ← `(command| #guard_msgs in section)
logInfo stxwould be completely unlinted?
Just to be explicit, I am happy with the change, just testing how far the consequences stretch! 😄
There was a problem hiding this comment.
You are correct, this change is at odds with the #-command linter. One idea that comes to mind is that we could have a core linter against #guard_msgs itself and enable it for mathlib, but I need to think about this more.
There was a problem hiding this comment.
This is not an issue for Mathlib: the #-command linter checks the kind of the command on the nose (no digging inside the syntax, as far as I remember). Thus #guard_msgs actually appears as an in to that linter and #guard_msgs is not linted.
There was a problem hiding this comment.
I'm a bit confused about what you're saying — could you take a look at the log for the mathlib testing branch? There's an error in test/HashCommandLinter.lean where #guard_msgs is supposed to be linted. This PR makes it so that #guard_msgs never has linters run on it, and this causes that test to fail.
I'm not sure what you mean about #guard_msgs appearing as an in; the in is part of its syntax, it's not Lean.Parser.Command.in.
There was a problem hiding this comment.
Part of my confusion was due to the fact that the error in the tests is not visible in VSCode, but only with lake test.
The other confusion is that I remembered that in shielded the #-command linter, but really it is the doc-string that usually accompanies #guard_msgs that makes the linter ignore #guard_msgs.
Hence, as is, it is hard for #guard_msgs to get caught in the #-command linter:
import Mathlib.Tactic.Linter
--flagged
#guard_msgs in
run_cmd return
-- not flagged
/---/
#guard_msgs in
run_cmd return
-- not flagged
/-- info: 0 -/
#guard_msgs in
#eval 0This behaviour was partly by design. I would be happy to have #guard_msgs flagged more consistently as a #-command, but also to make it maintain "special status".
There was a problem hiding this comment.
Thanks for your feedback @adomani, it's helpful to know that you are ok with #guard_msgs being special like this. We can revisit being able to lint for #guard_msgs in mathlib if that ever comes up.
Would you mind fixing that first mathlib HashCommandLinter.lean test as a mathlib PR? That will help with the next nightly-testing.
There was a problem hiding this comment.
I'm going to fix the test in the same lean-pr-testing-5644 branch, right?
There was a problem hiding this comment.
I don't think it's necessary to fix lean-pr-testing-5644. Maybe all we need to do is fix the nightly-testing branch of mathlib directly.
Pinging @jcommelin: My understanding is that in the next nightly, we'll have to fix the first test in HashCommandLinter.
There was a problem hiding this comment.
Ok, I have added the fix to lean-pr-testing-5644 and I also removed the "hacky pairs" of set_option ... false #guard_msgs in set_option ... true in ....
I can cherry-pick these changes to the appropriate nightly PR, though.
|
Note to self/whoever gets to address this first: when this lands, batteries also has such as hack which can be removed now. |
leanprover-community-bot
added
builds-mathlib
The
#guard_msgscommand runs the command it is attached to as if it were a top-level command. This is because the top-level command elaborator runs linters, and we are interested in capturing linter warnings using#guard_msgs. However, the linters will run on#guard_msgsitself, leading sometimes to duplicate warnings (like for the unused variable linter).Rather than special-casing
#guard_msgsin every affected linter, this PR special-cases it in the top-level command elaborator itself. Now linters are only run if the command doesn't contain#guard_msgs. This way, the linters are only run on the sub-command that#guard_msgsruns itself. This rule also keeps linters from running multiple times in cases such asset_option pp.mvars false in /-- ... -/ #guard_msgs in ....