pointless tactic linter

Stream: general

[Damiano Testa]

I just opened #11308 with a "pointless tactic linter": the linter inspects the goals before and after each tactic and emits a warning if it detects no change.

The PR also contains some of the tactic-removals arising from the linter.

If you have any comments, I'd be happy to hear them!

(Also, I am not done removing the pointless tactics and there is some decision to be taken about explicit skips in the code.)

[Damiano Testa]

As this PR gets discussed, it is probably a good idea to agree on a few style guidelines.

Here is a first question: should the linter flag tactics like done and skip? If you have an opinion give :thumbs_up:/:thumbs_down: for support/rejection and whichever other emoji you want for whatever else you want to express!

[Damiano Testa]

I personally find done very good pedagogically, but I probably prefer it to not appear in Mathlib (unless nolinted).

[Damiano Testa]

With skip, ideally I would like to flag uses of skip such as

example : True := by
  skip
  exact .intro

(of which the linter found quite a few!). I would rather it not flag uses of skip as in ... <;> [skip, ring]; aesop. However, I am not sure how to achieve both in a robust way.

[Damiano Testa]

I would rather uses of skip be flagged by the linter.

[Mario Carneiro]

The point of a linter is to suggest a modification which it thinks is better. (Ideally with a code action to perform it.) If it can't find a way to express that modification, then it should probably just be quiet.

Applying this principle to the <;> [skip; ring] case, the basic idea is that useless tactics can only be removed from a tacticSeq if there is more than one tactic in the seq (otherwise it would result in an erroneous 0-tactic list), and tactics appearing where a tactic is expected can't be removed at all, and can at best be replaced by skip. So you should flag useless tactics in a tacticSeq if they are either not the only thing in the list, or if they are not skip.

[Damiano Testa]

Mario, that clarifies a lot, thanks! I'll try to make the linter aware of the ranges of tacticSeq and update its behaviour accordingly.

[Damiano Testa]

1. Given the vote above, I have decided that done, by default triggers a warning. If there is a strong differing opinion, changing this decision is simply a matter of adding done to the already existing whitelist.

[Damiano Testa]

2. I made the linter not inspect seq_focus blocks altogether. It is true that there could be some really unused tactics inside there, but I think that entering seq_focus is a task for a second pass!

[Damiano Testa]

3. As mathlib is almost compliant with the unused tactic linter, I am looking at whether the linter should also act on tests. I suspect that it should, since getting feedback about whether a tactic is or isn't doing something is valuable. However, inside test, I am finding it hard to not whitelist a lot of tactics.

[Damiano Testa]

So, should tests be "unused tactic linted"?

[Damiano Testa]

A possibility is always to disable the unused tactic linter inside tests and everyone can opt in via set_option linter.unusedTactic true.

[Mario Carneiro]

Damiano Testa said:

A possibility is always to disable the unused tactic linter inside tests and everyone can opt in via set_option linter.unusedTactic true.

I would recommend the opposite: you should use this set_option in every test that involves unused tactics

[Damiano Testa]

Ok, I will make the linter act everywhere.

I will add fail_if_success and its friends to the whitelisted tactics, though, right? Those seem to already have their own control of what should work/not work, so, in some sense are already taking over what the blanket "unused tactic" would do.

[Mario Carneiro]

yeah, fail_if_success should be whitelisted, since there is basically no reason to use it for an effect accidentally

[Mario Carneiro]

I mean I suppose it's conceivable that someone could have written it in a proof and it isn't doing anything, but most likely such a proof is for teaching or demonstration purposes anyway, and flagging it won't be useful

[Mario Carneiro]

although that does relate to a potential issue with linters like this, which is that it is difficult for downstream projects to disable it globally

[Mario Carneiro]

e.g. if they want to use done

[Damiano Testa]

Would it make sense to store a local file with the whitelist and the tactic parses that file to know which tactics to whitelist and which ones to check? That would make customizable what you want and do not want to use.

[Damiano Testa]

The linter is now green!

I wrote a summary of the files touched by the PR in the description and the linter comes with its documentation.

Essentially, even though the PR touches 23 files,

• 17 are for set_options in tests,
• 1 is the file with the linter,
• 3 are noshake and the Mathlib and Mathlib.Tactic additions,
• 1 is the file to import the linter early in the hierarchy,
• 1 is the file in Mathlib that opts out of the linter!

[Thomas Murrills]

Damiano Testa said:

Ok, I will make the linter act everywhere.

I will add fail_if_success and its friends to the whitelisted tactics, though, right? Those seem to already have their own control of what should work/not work, so, in some sense are already taking over what the blanket "unused tactic" would do.

Could the whitelisted parsers just be tagged with an attribute instead of stored in a list, e.g. @[allow_unused_tactic]? (It might be easy to spin one up with register_label_attr.)

[Damiano Testa]

I was thinking the same, but, since I never wrote anything involving an attribute, I did not want to slow down the PR.

[Damiano Testa]

Also, it is something that can be added after the linter is in place, so it did not seem urgent. I would be happy to take the opportunity to learn about attributes, though!

[Damiano Testa]

(This does not appear from the current status of the PR, but over 100 files had unused tactics, so, at the beginning, it was not clear how long it would take to fix everything! :smile:)

[Thomas Murrills]

Aside: I've been handling some attribute and environment extension stuff lately, and I don't want to keep all that I've learned to myself—I wonder if it would be alright to start a page in the mathlib4 wiki on attributes where I could develop a sort of "how to write an attribute" piece. (I notice that the lean manual and metaprogramming book don't seem to cover attributes in an in-depth fashion yet.)

[Damiano Testa]

I was thinking of doing something analogous for linters...

[Damiano Testa]

I do not know about others, but I found those wiki pages very helpful. In particular, I've consulted the monads page more than I would like to admit... :smile:

[Yaël Dillies]

Thomas Murrills said:

Could the whitelisted parsers be tagged with an attribute instead of stored in a list, e.g. @[allow_unused_tactic]?

Please don't write one attribute per linter!

[Damiano Testa]

One attribute to lint them all...

[Thomas Murrills]

Yaël Dillies said:

Thomas Murrills said:

Could the whitelisted parsers be tagged with an attribute instead of stored in a list, e.g. @[allow_unused_tactic]?

Please don't write one attribute per linter!

You mean write more than 1 attribute per linter? :open_mouth: (Just kidding. :P )

[Thomas Murrills]

I think a label attribute is pretty lightweight and low-maintenance here! Here's the entirety of how it might look:

import Lean

register_label_attr allow_unused_tactic

open Lean Elab Command in
/-- Gets the array of tactic nodekinds which are allowed to be unused. -/
def getAllowedUnusedTacKinds : CommandElabM (Array Name) :=
  liftCoreM <| labelled `allow_unused_tactic

(the monad of labelled should be lowered to IO, I think—then we wouldn't need liftCoreM.)

Though I haven't looked closely at the PR yet.

[Damiano Testa]

If I am following what you are saying, the SyntaxNodeKinds of the tactics that are allowed to be unused would be stored in the environment, so that the linter could dynamically pick them up as it goes through the declarations, right?

This makes me think that the monad should have access to the environment, though and so this may rule out IO, maybe?

[Mario Carneiro]

I think there is already a setup for this in the unreachable tactic linter

[Mario Carneiro]

it uses the really-super-basic version of an attribute: there is an IO ref and you use initialize to add things to it

[Damiano Testa]

Ok, the part with initialize I did copy, but I did not understand it much. So, from what you are saying, not only it is in the unreachable tactic, but it is actually also already in the unused tactic linter! :upside_down:

[Mario Carneiro]

the way to add something to it would be

initialize addIgnoreTacticKind ``tacticStx

[Damiano Testa]

Ok, let me try

[Mario Carneiro]

The unnecessary seq focus uses a slightly heavier weight version, a TagAttribute which is basically what is suggested above. So you would tag a tactic you don't want linted as @[multigoal]

[Mario Carneiro]

Both versions also come with a list of "builtins" which come pre-tagged

[Mario Carneiro]

this is necessary for the TagAttribute case because you can't tag something in another file

[Damiano Testa]

Ok, I think that there is something that I am not understanding now and it is also getting late here: I'll sleep on it and will get back to it later!

In the meantime, the linter may already be extendable, without me being able to extend it! :smile:

[Thomas Murrills]

(And by the way: a label attribute is just meant to be a tag attribute which lets you add labels in other files! It's also implemented slightly differently, though.)

[Mario Carneiro]

The major advantage of the attributes with the same-file restriction is that they have zero overhead at import time. Just remember that if you use any initialize code then that code runs whenever someone does import Mathlib for each and every tagged definition...

[Thomas Murrills]

Hmm—in principle, is the lack of overhead intrinsic to the same-file restriction? (I do see that label attributes use a scoped env extension, which it’s clear has more overhead in general, though.)

I’m not totally clear on what’s special about adding a declaration to the extension while in the same module as opposed to otherwise. (There might be a clue in the fact that we have both addEntryFn and addImportedFn, and the latter is constant for tag attributes…but it’s not clear to me how and why it can get away with being constant.)

[Mario Carneiro]

Hmm—in principle, is the lack of overhead intrinsic to the same-file restriction? (I do see that label attributes use a scoped env extension, which it’s clear has more overhead in general, though.)

The way they are related is that there are the following options for lookup into an extension:

1. Find the file containing the declaration -> check the extension map for that file to see if the declaration is marked
2. Search all extension maps to see if the declaration is marked in any of them
3. Merge extension maps on import, then look up into the merged map

Option 1 is only correct if you have the same file restriction. Option 2 is expensive at lookup time, which usually disqualifies it from consideration. Option 3 has import-time overhead. TagDeclarationExtension uses option 1, while ScopedEnvExtension uses option 3.

[Thomas Murrills]

Oh, ok, makes sense! (The existence of extension maps for files in the first place was my blind spot. I can understand why we’d want to hide them under abstractions, though.)

I suppose one other option (maybe) (in principle) is that we could always also search the extension map for one other specific “initial” file (specified when the extension was registered). That would let us “start off” by tagging a bunch of declarations.

(Or a more generic hybrid approach where we dynamically keep track of a list of modules that add tags to decls from other modules, then just merge those modules’ extension maps, and fallback to lookup in that merged map if lookup-by-original-module fails. Not sure if this would actually be needed by anything though.)

[Mario Carneiro]

(The existence of extension maps for files in the first place was my blind spot. I can understand why we’d want to hide them under abstractions, though.)

Well, it's not necessarily a map; extensions can put basically whatever they like in a .olean file. The constraint is that you have to prepare that data structure per-file and while they get loaded from disk for ~free using mmap, any processing of the data is going to add overhead at import time, so the best thing you can do is just leave that data as is and consult it later. Of course we still have the import-time overhead of producing the constant map of the Environment, but that's pretty fundamental to lean so it's unlikely we can avoid that cost.

[Mario Carneiro]

I suppose one other option (maybe) (in principle) is that we could always also search the extension map for one other specific “initial” file (specified when the extension was registered). That would let us “start off” by tagging a bunch of declarations.

That's what TagAttributeExtra implements. More precisely, it augments a TagAttribute with a hard-coded list of declarations that are consulted if the lookup in option (1) fails.

[Mario Carneiro]

(Or a more generic hybrid approach where we dynamically keep track of a list of modules that add tags to decls from other modules, then just merge those modules’ extension maps, and fallback to lookup in that merged map if lookup-by-original-module fails. Not sure if this would actually be needed by anything though.)

I don't think this works, because how would you know whether a module is "of interest" and in need of merging unless you look inside it? Or maybe the idea is more that it's actually two extensions (or behaves roughly like that), and you only use the "expensive" extension for cross-module entries. I think that would be useful as an optimization of many of mathlib's extensions which use the more heavyweight extensions because of the fewer restrictions even though it is rare to actually make use of the mechanism.

[Thomas Murrills]

The implementation I had in mind was something like: “store the names of modules with cross-module entries in an auxiliary “merge-style” extension” (with the hope that most modules won’t contribute their name and so merging to obtain this list of names will be efficient(?)), then for the decls we actually care about, either: “try module-of-origin lookup, and if that fails, look in each listed module in turn” or instead “merge the entries from each listed module at import time, then lookup based on module of origin, and fall back to the merged data if that fails”. Though I don’t know how the costs compare.

But at that point (in the second option), I guess your notion is that you might not really need the list in the first place (depending on how the implementation shakes out) and this is basically equivalent to two [parallel, internal] extensions!

[Thomas Murrills]

Mario Carneiro said:

I suppose one other option (maybe) (in principle) is that we could always also search the extension map for one other specific “initial” file (specified when the extension was registered). That would let us “start off” by tagging a bunch of declarations.

That's what TagAttributeExtra implements. More precisely, it augments a TagAttribute with a hard-coded list of declarations that are consulted if the lookup in option (1) fails.

Oh, nice! I wonder if that would be appropriate for this linter—I suppose it depends on whether you can still erase the hardcoded tags locally. (But I’m on mobile right now, so can’t easily check.)

[Thomas Murrills]

(Wait, you can erase tag attributes, at least in a way that doesn’t persist over imports, right? I’m figuring that would just be an addition to some erased collection in the environment, as usual, not something written to oleans. But I haven’t checked that TagAttribute(Extra)s actually implement erasure.)

[Mario Carneiro]

Thomas Murrills said:

Wait, you can erase tag attributes, at least in a way that doesn’t persist over imports, right?

No, at least not currently. There is nothing fundamentally preventing this but it's not implemented.

[Damiano Testa]

I !benched the PR and it is incredibly slow!

[Damiano Testa]

Maybe this is a topic for testing linters more generally, but I wanted to add a test file, delimiting some of the boundaries of the linter.

I can certainly put in tests for tactics that are allowed to not make progress -- that's easy.

However, #guard_msgs does not seem to catch the warnings thrown by the linter, so I do not know how to produce a quiet test verifying, for instance this:

/--
warning: 'skip' tactic does nothing [linter.unusedTactic]
-/
#guard_msgs in
example : True := by
  skip  -- the warning is still here!
  exact .intro

[Damiano Testa]

For a minimized example, this suffers from the same issue:

/-- warning: unused variable `n` [linter.unusedVariables] -/
#guard_msgs in
example (n : Nat) : True := .intro -- warning is still here

[Mario Carneiro]

see https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.23guard_msgs.20doesn't.20silence.20warnings

[Damiano Testa]

A low key solution could be to have part of the test files to allow warnings but not errors and use #guard_msgs there.

[Damiano Testa]

If anyone is looking for a speeding up opportunity, the linter at #11308 causes an 8.5% slowdown (see this !bench).

I found that the linter worked well, in that it caught several tactics that were not actually doing anything. The only possible problem that I can see with it, is the slow down. Honestly, though, I do not really know what interpretation really means.

[Mario Carneiro]

interpretation is time in the lean interpreter, i.e. running your code

[Mario Carneiro]

You could use a hashset for allowed

[Mario Carneiro]

also I think you should make swap_var an allowed tactic, I doubt the bespoke check is worth it

[Mario Carneiro]

The structure of the unused tactic linter is also not optimal for this job because you don't care about tactics that are never executed, so you can just look at tacticinfo nodes and not worry about syntax

[Damiano Testa]

Mario, thanks a lot for your comments!

I was thinking that maybe it makes sense to merge the unreachable and unused tactic linters: do you think that it would be an improvement?

[Damiano Testa]

Mario Carneiro said:

You could use a hashset for allowed

This is mostly for developing my intuition: you think that making allowed a HashSet might have a measurable speed improvement?

[Mario Carneiro]

yes

[Mario Carneiro]

because on every tactic you are checking against allowed and failing it is the common case, so that's 1 hash check vs 15 or so equality checks