Persistent #allow_unused_tactic

Stream: mathlib4

[Patrick Massot]

It seems that #allow_unused_tactic that allows to silence the unused tactic linter does not work across files. I want to define a tactic and make sure it is never flagged.

[Patrick Massot]

Is this possible?

[Patrick Massot]

Actually, the unxy-ed version is I would be very happy if this linter would consider that anything that changes the tactic state is used, even if it is the same up to defeq. The current implementation of the linter explicitly whitelists change.

[Johan Commelin]

cc @Damiano Testa

[Damiano Testa]

First, an answer the original question.

I had thought about making a persistent #allow_unused_tactic: I think that this would be useful at least downstream. For instance, I used by ... done when I teach and right now I have to allow done in every file.

[Damiano Testa]

The persistent version could be implemented by adding an environment extension that stores the unused tactics that are allowed. This would mean that docs#Mathlib.Tactic.allowedRef (the IO.Ref that currently stores the allowed tactics) could be removed in favour of a dynamic implementation, by allowing each tactic at the point of definition, rather than up front, when the linter is defined.

[Damiano Testa]

I still think that the current file-only exclusion is valuable, so my preference would be to add #allow_unused_tactic! that is persistent, while keeping also the current #allow_unused_tactic unchanged.

[Damiano Testa]

For the second part, the implementation does not actually use isDefEq, but looks at whether there is a change in the list of metavariables (i.e. their name) and tactics such as change actually do modify the metavariable.

[Damiano Testa]

Can you give an example of a situation where you would like the linter to not flag a tactic as unused? I would probably consider this a bug in the linter, rather than a tactic that should be allowed.

[Damiano Testa]

In fact, #20412 removes change from the allowed tactics: let's see if the linter flags something that it should not in mathlib!

[Damiano Testa]

I just looked at the first 3 exceptions flagged by the linter with change being in scope, and they are all situations where the infoview shows no difference.

[Damiano Testa]

I went through all the exceptions and they were all situations where the infoview showed no difference before and after change.

[Damiano Testa]

In one situation, this allowed the removal of a porting note.

[Damiano Testa]

The PR above incorporates also the cleanup.

[Johan Commelin]

Looks great!

[Patrick Massot]

Thanks Damiano! I’m very happy that this question helped cleaning up a bit.

[Damiano Testa]

Patrick, are you still interested in the persistent form of #allow_unused_tactic?

[Patrick Massot]

Sure!

[Patrick Massot]

I cannot really check that the latest change to the linter is enough for me because I haven’t updated Verbose Lean to Lean 4.15.0-rc1 because of the token issue with white spaces.

[Patrick Massot]

But I’m sure this is a useful command anyway.

[Damiano Testa]

You mentioned a custom tactic: maybe you could test on Mathlib's master where you add a stub of your tactic.

[Damiano Testa]

(However, the current version of #allow_unused_tactic is certainly not persistent and it only works in the file where it is written.)

[Damiano Testa]

With respect to the persistent unused tactic issue: should I completely remove the current exceptions IO.Ref, in favor of extending the to-be-created environment extension?

[Patrick Massot]

Mathlib master doesn’t help with

import Mathlib.Tactic

open Lean Parser Elab Tactic

macro "rename_bvar' " old:ident " → " new:ident loc?:(location)? : tactic =>
  `(tactic|rename_bvar $old → $new $[$loc?]?)

set_option linter.unusedVariables false

example (n : ℤ) (hnk : ∃ k, n = 2 * k + 1) : True := by
  rename_bvar' k → l at hnk
  trivial

[Patrick Massot]

Using rename_bvar instead of rename_bvar' works because it is whitelisted.

[Damiano Testa]

#20438 implements the persistent version of #allow_unused_tactic. The PR contains both versions:

• #allow_unused_tactic ids, the non-persistent command that is already in Mathlib;
• #allow_unused_tactic! ids the persistent command that is new to the PR.

[Damiano Testa]

The persistence is achieved through an environment extension, which means that in order to use it, it needs to be in a separate file. All of Mathlib serves as a test for persistence, since I used #allow_unused_tactic! ids for a few tactics that before were in the IO.Ref.

[Damiano Testa]

Besides moving code around, the PR basically introduces the extension and uses it almost minimally. I opted for not moving the exceptions to the files where the tactics are defined.

[Damiano Testa]

If this is something that is used frequently, then maybe we can also think a little about how to input the tactics that should be ignored: the SyntaxNodeKind is not really how I would identify a tactic and there is a layer of obscurity between wanting to allow refine to be unused and realizing that it is really Lean.Parser.Tactic.refine that should be used.

[Damiano Testa]

Even something as simple-minded as

elab "#show_kind " t:tactic : command => do
  let stx ← `(tactic| $t)
  Lean.logInfo m!"The `SyntaxNodeKind` is '{stx.raw.getKind}'"

--  The `SyntaxNodeKind` is 'Lean.Parser.Tactic.refine'
#show_kind refine _

could be useful.

[Patrick Massot]

Ironically, this PR doesn’t pass linting CI.

[Patrick Massot]

I also realized from the other thread that I probably want to simply disable (all?) linters in my course material.

[Damiano Testa]

I pushed what I think is a fix for the linting!

[Damiano Testa]

CI passed and I also added the #show_kind command to the PR.

[Damiano Testa]

The persistent form of #allow_unused_tactic just made it into mathlib master. Using

#allow_unused_tactic!
  Lean.Parser.Tactic.done
  Lean.Parser.Tactic.skip

should make the linter ignore done and skip from where the command is issued onwards, also on files imported by the file where the command is issued.