Special-casing the unusedTactic linter

Stream: mathlib4

[Heather Macbeth]

(For some reason the unusedTactic linter objects to one version's test file but not the other, has anyone debugged this kind of unpredictability before?)

[Damiano Testa]

Just glancing at the code (I am not at a computer), I think that the linter is complaining about the "config" skip that the linter considers to be unused.

[Heather Macbeth]

Right, but there is an identical file in which no complaints occur.

[Damiano Testa]

Oh, on which file is the linter silent?

[Heather Macbeth]

It's noisy on test/linear_combination' and silent on test/linear_combination :)
https://github.com/leanprover-community/mathlib4/actions/runs/10566534579/job/29273542575

[Damiano Testa]

Ah, the docs of the linter hold the answer:

* The tactic does not check the discharger for `linear_combination`,
  but checks `linear_combination` itself.
  The main reason is that `skip` is a common discharger tactic and the linter would
  then always fail whenever the user explicitly chose to pass `skip` as a discharger tactic.

[Damiano Testa]

So, I am guessing that linear_combination' should be special-cased in the same way.

[Heather Macbeth]

Aha! Thanks!

[Damiano Testa]

I can do that tomorrow, but if you want to take care of it now, it should be pretty straightforward as a change.

[Heather Macbeth]

I made a guess on how to fix it, and if I guessed correctly, there will be no need to bother you.

[Notification Bot]

10 messages were moved here from #mathlib4 > Narrowing the scope of linear_combination by Heather Macbeth.

[Michael Rothgang]

I think the guess is almost right; it should be

``|>.insert `Mathlib.Tactic.LinearCombination'.linearCombination'``

[Michael Rothgang]

(The namespace name also has a prime.)

[Mario Carneiro]

@Damiano Testa that sounds like another instance of that principle from before: skip when used as a tactic (rather than a tacticSeq), or as the lone tactic in a tacticSeq, shouldn't be linted because you can't syntactically delete it

[Damiano Testa]

Where is the information of whether the syntax is a tactic or a tacticSeq? I imagine somewhere in the infotree, but I cannot seem to find it.

[Mario Carneiro]

it's in the syntax itself

[Mario Carneiro]

although in general it's not super easy to get a hold of

[Mario Carneiro]

the parent syntax will have some expectation for what its child is

[Damiano Testa]

Stored in... preresolved?

[Damiano Testa]

Or the SourceInfo?

[Mario Carneiro]

no, just the structure of the tree and the node names

[Damiano Testa]

I am looking at what I thought was the "whole" syntax tree and I cannot find it.

[Mario Carneiro]

in the case of tacticSeq, you can more or less what the hard code the possible parents are

[Damiano Testa]

Ah, like a missing null node somewhere?

[Mario Carneiro]

I mean if the parent is a tacticSeqIndented node and under that is a null node and under that is a bunch of syntax nodes, then all those syntax nodes are in the tactic category because that's what tacticSeqIndented expects

[Damiano Testa]

Got it: it is a "usual" skip that appears inside something that was parsed as a tacticSeq or not.

[Mario Carneiro]

If it is a skip node and its parent is a null node of length 1 (whose parent is a tacticSeqIndented or tacticSeqBracketed node), then that means it's alone in its tacticSeq

[Mario Carneiro]

if it has a parent that isn't a null node then it is being used as a tactic directly in some other syntax

[Damiano Testa]

Indeed: this is what a skip with usual tactic parsing looks like

|-node linearCombination, none
|   |-atom original: ⟨⟩⟨ ⟩-- 'linear_combination'
|   |-node null, none
|   |   |-node normStx, none
|   |   |   |-atom original: ⟨⟩⟨⟩-- '('
|   |   |   |-atom original: ⟨⟩⟨ ⟩-- 'norm'
|   |   |   |-atom original: ⟨⟩⟨ ⟩-- ':='
|   |   |   |-node Lean.Parser.Tactic.skip, none
|   |   |   |   |-atom original: ⟨⟩⟨⟩-- 'skip'
|   |   |   |-atom original: ⟨⟩⟨⏎  --rfl⏎⏎⟩-- ')'
|   |-node null, none

and this is what it looks like when you modify linear_combination to use a tacticSeq as discharger:

|-node linearCombination, none
|   |-atom original: ⟨⟩⟨ ⟩-- 'linear_combination'
|   |-node null, none
|   |   |-node normStx, none
|   |   |   |-atom original: ⟨⟩⟨⟩-- '('
|   |   |   |-atom original: ⟨⟩⟨ ⟩-- 'norm'
|   |   |   |-atom original: ⟨⟩⟨ ⟩-- ':='
|   |   |   |-node Lean.Parser.Tactic.tacticSeq, none
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, none
|   |   |   |   |   |-node null, none
|   |   |   |   |   |   |-node Lean.Parser.Tactic.skip, none
|   |   |   |   |   |   |   |-atom original: ⟨⟩⟨⟩-- 'skip'
|   |   |   |-atom original: ⟨⟩⟨⏎  --rfl⏎⏎⟩-- ')'

[Damiano Testa]

After the := I can now see that the syntax either places directly the node for the tactic or starts the dance for a tacticSeq.

[Mario Carneiro]

in this case, you want to lint only when it has a parent that is a tacticSeq with more than 1 element

[Mario Carneiro]

so both of these cases would be rejected

[Damiano Testa]

Yes, agreed.

[Damiano Testa]

"Rejected" as in "allowed by the linter"! :upside_down:

[Mario Carneiro]

although if the tactic is anything other than skip you still want to lint it and suggest to replace it by skip in these edge cases

[Damiano Testa]

Yes, I am not sure that I will have time to work on this this week, but I agree: a tactic (that is not part of a tacticSeq!) should not be linted and a tacticSeq should be linted only if it contains more than one tactic.

[Damiano Testa]

From an "efficiency" point of view, does it make sense to make the linter not inspect tactics that are required to modify something? E.g., should the linter not inspect simp in all its forms or is it not worth it?

[Mario Carneiro]

simp can have the failIfUnchanged := false option, in which case it may not fail even if it does nothing