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 tactics 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