Zulip Chat Archive
Stream: triage
Topic: PR !4#19556: perf: disable the unused tactic linter
Random Issue Bot (Jan 03 2025 at 14:11):
Today I chose PR 19556 for discussion!
perf: disable the unused tactic linter
Created by @None (@grunweg) on 2024-11-28
Labels: WIP, t-linter, awaiting-bench
Is this PR still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Jan 03 2025 at 15:32):
@Damiano Testa Given your recent work on this linter, is this issue still relevant?
Damiano Testa (Jan 03 2025 at 15:32):
I think that it is still relevant: most linters that I wrote that scan InfoTrees
should be optimized. This is something that I know and that I plan to do.
Damiano Testa (Jan 03 2025 at 15:33):
For the specifics of the unused tactic linter, I think that an optimization would be to try and merge it with the multigoal linter: that may roughly half the cost of running both, with very little thought about how to actually optimize them!
Damiano Testa (Jan 03 2025 at 15:34):
(And it would also mean that any future optimization only needs to be implemented once.)
Patrick Massot (Jan 03 2025 at 15:59):
Are there instructions somewhere to completely disable linters in a lib depending on Mathlib? I really don’t want my students to spend CPU power on linting.
Damiano Testa (Jan 03 2025 at 17:03):
Would your students be cloning a repository that you set up for them, or would they be creating one on their own?
Damiano Testa (Jan 03 2025 at 17:04):
A way of silencing the linters is to set their (weak) options in the lakefile to false
: this works well if they are all cloning the same repository, since then you just plant this set up once.
Damiano Testa (Jan 03 2025 at 17:05):
A more principled approach though, would be to have an "option to rule them all": every linter runs only if its specific option is true
and the "all linters option" is also true
.
Damiano Testa (Jan 03 2025 at 17:06):
Then, in downstream projects, you only need to set the "all linters option" to false to achieve silencing and you do not need to worry about new linters appearing in the future.
Damiano Testa (Jan 03 2025 at 17:06):
This second alternative is not available at the moment, though.
Patrick Massot (Jan 03 2025 at 18:37):
They will use my repo. That course has no interaction with git at all.
Damiano Testa (Jan 03 2025 at 19:00):
So, an easy solution is to copy the weak options from mathlib's lakefile and set them all to false.
Eric Wieser (Jan 03 2025 at 19:23):
Running run_cmd Lean.Elab.Command.lintersRef.set #[]
also disables all linters including builtin ones, until you next relaunch the lean server
Patrick Massot (Jan 03 2025 at 20:01):
Thanks for the explanation!
Patrick Massot (Jan 15 2025 at 15:47):
I’m getting back to this because I can’t make it work. Can anyone share a lakefile.toml
which disables all linters in a project depending on Mathlib? If this is too complicated, I would already be happy with disabling the unused tactic linter. @Damiano Testa
Patrick Massot (Jan 15 2025 at 15:48):
It really really doesn’t help that lake is silently ignoring every section of lakefile.toml
that actually doesn’t exist.
Michael Rothgang (Jan 15 2025 at 17:36):
Here's one for just hte unused tactic linter; full example upcoming
name = "«mathlib-tryforeachstep-test»"
defaultTargets = ["MathlibTryforeachstepTest"]
[leanOptions]
pp.unicode.fun = true
linter.unusedTactic = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
[[lean_lib]]
name = "MathlibTryforeachstepTest"
Michael Rothgang (Jan 15 2025 at 17:41):
Updated version: you may consider if the refine
, oldObtain
or style.multiGoal
linters are actually beneficial.
name = "«mathlib-tryforeachstep-test»"
defaultTargets = ["MathlibTryforeachstepTest"]
[leanOptions]
pp.unicode.fun = true
autoImplicit = false
linter.unusedTactic = false
linter.hashCommand = false
linter.oldObtain = false
linter.refine = false
linter.style.cdot = false
linter.style.dollarSyntax = false
linter.style.header = false
linter.style.lambdaSyntax = false
linter.style.longLine = false
linter.style.missingEnd = false
linter.style.setOption = false
linter.style.multiGoal = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
[[lean_lib]]
name = "MathlibTryforeachstepTest"
Michael Rothgang (Jan 15 2025 at 17:42):
(This is on the current version of mathlib. I'm pretty sure it should also work on 4.15.0, but haven't tested that.)
Patrick Massot (Jan 15 2025 at 18:10):
Thanks a lot for trying to help Michael, but it simply does not work.
Damiano Testa (Jan 15 2025 at 20:02):
Patrick, does Michael's approach work for the linters whose default value is false
in mathlib, but are then turned on within all of mathlib as weak
options?
Damiano Testa (Jan 15 2025 at 20:03):
Alternatively, do you want to disable completely the unusedTactic linter in mathlib, or having the persistent exclusion of certain tactics be enough?
Michael Rothgang (Jan 15 2025 at 20:24):
Right, I should have tested locally... does the following work? (It works for me locally, in the sense that lake build
passes.)
name = "«mathlib-tryforeachstep-test»"
defaultTargets = ["MathlibTryforeachstepTest"]
[leanOptions]
pp.unicode.fun = true
autoImplicit = false
weak.linter.unusedTactic = false
weak.linter.hashCommand = false
weak.linter.oldObtain = false
weak.linter.refine = false
weak.linter.style.cdot = false
weak.linter.style.dollarSyntax = false
weak.linter.style.header = false
weak.linter.style.lambdaSyntax = false
weak.linter.style.longLine = false
weak.linter.style.missingEnd = false
weak.linter.style.setOption = false
weak.linter.style.multiGoal = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
[[lean_lib]]
name = "MathlibTryforeachstepTest"
Patrick Massot (Jan 15 2025 at 21:41):
lake doesn’t complain but the linter still run
Patrick Massot (Jan 15 2025 at 21:41):
I see this unused tactic linter more and more like a virus.
Damiano Testa (Jan 15 2025 at 21:47):
Do the other linters whose default option is false also run?
Patrick Massot (Jan 15 2025 at 21:49):
I’m not sure what the other ones are meant to do
Damiano Testa (Jan 15 2025 at 21:49):
What happens if you use set_option pp.all true
?
Patrick Massot (Jan 15 2025 at 21:50):
I see the expected verbose output of pp.all
Damiano Testa (Jan 15 2025 at 21:50):
Ah, no linter warning?
Patrick Massot (Jan 15 2025 at 21:52):
no
Damiano Testa (Jan 15 2025 at 21:53):
Ok, so maybe setting of weak
options only works when the default value of false
.
Damiano Testa (Jan 15 2025 at 21:54):
So, rather than disabling the linter for all of mathlib, we can disable it only for mathlib's dependencies and then the toml that Michael gave you should work.
Patrick Massot (Jan 15 2025 at 21:54):
I’m sorry but I have no idea what this sentence means.
Patrick Massot (Jan 15 2025 at 21:55):
Is this something that needs to be done in Mathlib?
Damiano Testa (Jan 15 2025 at 21:55):
Right now, the default value of the unused tactic linter is true
, since it was decided that it was a useful enough linter that is should be on by default in mathlib's dependencies.
Michael Rothgang (Jan 15 2025 at 21:55):
I think it means: "A short PR to mathlib, which Damiano can quickly write and Michael can review quickly." (I can confirm that I'll be happy to review.)
Patrick Massot (Jan 15 2025 at 21:55):
For me Mathlib is frozen for one year.
Damiano Testa (Jan 15 2025 at 21:55):
However, for your course, this decision seems to be wrong.
Patrick Massot (Jan 15 2025 at 21:55):
For my teaching
Patrick Massot (Jan 15 2025 at 21:56):
It’s too late the deb file went to the IT guys
Damiano Testa (Jan 15 2025 at 21:56):
So, to allow you to teach, we can disable the linter for all mathlib's dependencies, but we can still have the linter on in mathlib, at least.
Michael Rothgang (Jan 15 2025 at 21:56):
Ok, so switching to a different branch of mathlib is not possible any more?
Damiano Testa (Jan 15 2025 at 21:56):
Patrick Massot said:
For me Mathlib is frozen for one year.
Ah, I did not realize this.
Patrick Massot (Jan 15 2025 at 21:57):
My course starts next Wednesday. I’m already lucky to work in a math department where I can send a random deb file one week before classes start and get it deployed.
Patrick Massot (Jan 15 2025 at 21:57):
I was not expecting zombie linters.
Damiano Testa (Jan 15 2025 at 21:57):
I wonder whether there is something that can be done on your project, where parsing a file implies setting the linter option to false.
Patrick Massot (Jan 15 2025 at 21:58):
I will find a hack redefining the command to set the options
Damiano Testa (Jan 15 2025 at 21:58):
Is there some command that you always use at the start of each file?
Patrick Massot (Jan 15 2025 at 21:58):
So there is no real harm, but I think it reveals a serious issue in our setup.
Patrick Massot (Jan 15 2025 at 21:58):
There is no such command, but I can make one.
Damiano Testa (Jan 15 2025 at 21:58):
That command could be redefined to mean set_option ...
plus whatever the command really does.
Patrick Massot (Jan 15 2025 at 21:59):
Students already know they can ignore the import line at the top of each file.
Damiano Testa (Jan 15 2025 at 21:59):
Well, the command already exists: set_option linter.unusedTactic false
... :smile:
Patrick Massot (Jan 15 2025 at 21:59):
Thanks a lot for trying anyway.
Damiano Testa (Jan 15 2025 at 21:59):
I think that from this test it emerges that the weak
linter options only work when the default value of the linter is false
.
Damiano Testa (Jan 15 2025 at 22:00):
If the linter's default value is true
, it looks as though there is no way for downstream projects to set their own options.
Damiano Testa (Jan 15 2025 at 22:01):
For instance, the setOption
linter has false
as default value, but mathlib overrides this by setting a weak option to true
.
Damiano Testa (Jan 15 2025 at 22:01):
And this linter does not cause problems for your project.
Damiano Testa (Jan 15 2025 at 22:02):
However, the unusedTactic linter has default value true
and this seems to be the cause of the issue: downstream projects do not seem to have the opportunity to silence it, even if they set a weak option to false.
Patrick Massot (Jan 15 2025 at 22:02):
Do you remember how to write a macro with values in command
that actually runs several commands? I always need to look it up?
Patrick Massot (Jan 15 2025 at 22:02):
Also, do you know which other linters are slow to run?
Damiano Testa (Jan 15 2025 at 22:02):
Of the list above, the multiGoal
linter is slow as well.
Damiano Testa (Jan 15 2025 at 22:03):
(the multiGoal and unusedTactic are almost the same linter)
Damiano Testa (Jan 15 2025 at 22:03):
I thought that macros with multiple commands "just worked": let me try.
Patrick Massot (Jan 15 2025 at 22:04):
You’re right, I’m misremembering
Patrick Massot (Jan 15 2025 at 22:04):
It must be something else that complains in this multiple lines case.
Damiano Testa (Jan 15 2025 at 22:05):
Ok, here is a test anyway!
import Lean
macro "bonjour" : command => `(
set_option linter.unusedVariables false
set_option linter.unusedVariables false
)
-- warning here
example (n : Nat) : True := trivial
bonjour
example (n : Nat) : True := trivial
Damiano Testa (Jan 15 2025 at 22:06):
I think that merging multiple tactic
s has some funny business: there is tacticSeq
and tactic
and sometimes you have to be careful with the distinction.
Patrick Massot (Jan 15 2025 at 22:07):
Yes, it’s definitely fiddly with tactics
Damiano Testa (Jan 15 2025 at 22:08):
Multiple commands "should" not be chainable, but I think that Kyle mentioned to me some time ago that there is special support for parsing multiple commands anyway.
Damiano Testa (Jan 15 2025 at 22:09):
Btw, I think that the fact that weak
options do not override a default value of true
is at least unexpected as decision.
Patrick Massot (Jan 15 2025 at 22:12):
Is this something that Lean is doing or Mathlib? I have no idea where is the linter framework nowadays.
Patrick Massot (Jan 15 2025 at 22:12):
I’m sure I’ll learn tons of stuff by watching your talk. But as you can see I don’t have any time for LT this year :sad:
Damiano Testa (Jan 15 2025 at 22:12):
These are the core linters, it is not mathlib's doing.
Damiano Testa (Jan 15 2025 at 22:13):
My crazy busy period was last term, so I know how you feel!
Damiano Testa (Jan 15 2025 at 22:14):
(This specific linter is just in mathlib, but it uses the linter framework defined in core. And lake
is responsible for the weak
options, I think.)
Last updated: May 02 2025 at 03:31 UTC