PR !4#19556: perf: disable the unused tactic linter

Stream: triage

[Random Issue Bot]

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]

@Damiano Testa Given your recent work on this linter, is this issue still relevant?

[Damiano Testa]

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]

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]

(And it would also mean that any future optimization only needs to be implemented once.)

[Patrick Massot]

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]

Would your students be cloning a repository that you set up for them, or would they be creating one on their own?

[Damiano Testa]

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]

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]

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]

This second alternative is not available at the moment, though.

[Patrick Massot]

They will use my repo. That course has no interaction with git at all.

[Damiano Testa]

So, an easy solution is to copy the weak options from mathlib's lakefile and set them all to false.

[Eric Wieser]

Running run_cmd Lean.Elab.Command.lintersRef.set #[] also disables all linters including builtin ones, until you next relaunch the lean server

[Patrick Massot]

Thanks for the explanation!

[Patrick Massot]

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]

It really really doesn’t help that lake is silently ignoring every section of lakefile.toml that actually doesn’t exist.

[Michael Rothgang]

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]

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]

(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]

Thanks a lot for trying to help Michael, but it simply does not work.

[Damiano Testa]

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]

Alternatively, do you want to disable completely the unusedTactic linter in mathlib, or having the persistent exclusion of certain tactics be enough?

[Michael Rothgang]

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]

lake doesn’t complain but the linter still run

[Patrick Massot]

I see this unused tactic linter more and more like a virus.

[Damiano Testa]

Do the other linters whose default option is false also run?

[Patrick Massot]

I’m not sure what the other ones are meant to do

[Damiano Testa]

What happens if you use set_option pp.all true?

[Patrick Massot]

I see the expected verbose output of pp.all

[Damiano Testa]

Ah, no linter warning?

[Patrick Massot]

no

[Damiano Testa]

Ok, so maybe setting of weak options only works when the default value of false.

[Damiano Testa]

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]

I’m sorry but I have no idea what this sentence means.

[Patrick Massot]

Is this something that needs to be done in Mathlib?

[Damiano Testa]

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]

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]

For me Mathlib is frozen for one year.

[Damiano Testa]

However, for your course, this decision seems to be wrong.

[Patrick Massot]

For my teaching

[Patrick Massot]

It’s too late the deb file went to the IT guys

[Damiano Testa]

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]

Ok, so switching to a different branch of mathlib is not possible any more?

[Damiano Testa]

Patrick Massot said:

For me Mathlib is frozen for one year.

Ah, I did not realize this.

[Patrick Massot]

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]

I was not expecting zombie linters.

[Damiano Testa]

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]

I will find a hack redefining the command to set the options

[Damiano Testa]

Is there some command that you always use at the start of each file?

[Patrick Massot]

So there is no real harm, but I think it reveals a serious issue in our setup.

[Patrick Massot]

There is no such command, but I can make one.

[Damiano Testa]

That command could be redefined to mean set_option ... plus whatever the command really does.

[Patrick Massot]

Students already know they can ignore the import line at the top of each file.

[Damiano Testa]

Well, the command already exists: set_option linter.unusedTactic false... :smile:

[Patrick Massot]

Thanks a lot for trying anyway.

[Damiano Testa]

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]

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]

For instance, the setOption linter has false as default value, but mathlib overrides this by setting a weak option to true.

[Damiano Testa]

And this linter does not cause problems for your project.

[Damiano Testa]

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]

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]

Also, do you know which other linters are slow to run?

[Damiano Testa]

Of the list above, the multiGoal linter is slow as well.

[Damiano Testa]

(the multiGoal and unusedTactic are almost the same linter)

[Damiano Testa]

I thought that macros with multiple commands "just worked": let me try.

[Patrick Massot]

You’re right, I’m misremembering

[Patrick Massot]

It must be something else that complains in this multiple lines case.

[Damiano Testa]

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]

I think that merging multiple tactics has some funny business: there is tacticSeq and tactic and sometimes you have to be careful with the distinction.

[Patrick Massot]

Yes, it’s definitely fiddly with tactics

[Damiano Testa]

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]

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]

Is this something that Lean is doing or Mathlib? I have no idea where is the linter framework nowadays.

[Patrick Massot]

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]

These are the core linters, it is not mathlib's doing.

[Damiano Testa]

My crazy busy period was last term, so I know how you feel!

[Damiano Testa]

(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.)