unusedVariables

Stream: mathlib4

[Yaël Dillies]

Could we tone down the unusedVariables linter? It forbids me naming a variable I don't call by name even if it appears in other hypotheses.

import Mathlib.Data.Set.Basic

example {α : Type _} {s : Set α} : s ⊆ s := fun a ha ↦ ha
-- unused variable `a` [linter.unusedVariables]

I think that's a reasonable use case, as naming the variable makes the infoview nicer.

[Floris van Doorn]

I think you're intended to use a name that starts with an underscore if you want to name an unused variable.

import Mathlib.Data.Set.Basic

example {α : Type _} {s : Set α} : s ⊆ s := fun _a ha ↦ ha

[Chris Hughes]

I really don't like this unusedVariables linter for the following reasons.

• It makes the tactic state much less readable if I revisit a proof.
• Sometimes the names of variables gives information about the role they play. e.g. hx is about x and G is a group.
• Now that we have can give implicit arguments explicitly with List.nil (α := G), we should try to make sure the names are nice.
• Although we can use underscores to name variables, $things£ _are _more_ -difficult'' to_ _read_ -with +-punctuation_ &everywhere'
• We don't gain anything by using underscores.

What do other people think?

[Johan Commelin]

I think that maybe it should have an option so that it only complains about genuinely unused variables, like the mathlib3 linter.

[Johan Commelin]

A variable is not unused if it appears implicitly.

[James Gallicchio]

by using underscores do you mean using _G instead of G for unused variables to turn off the lint?

[Chris Hughes]

James Gallicchio said:

by using underscores do you mean using _G instead of G for unused variables to turn off the lint?

Yes

[Kevin Buzzard]

My feeling when writing lean 3 code is that sometimes I'm very happy to put in the _s and sometimes I just want to put in the variable names even if they're not needed, because I've used g and h above so many times and I want to call them g and h again in the code even if the unification algorithm can figure them out.

[James Gallicchio]

for programming it's a pretty essential lint, but I can see mathlib wanting to turn it off/make it less aggressive

[Johan Commelin]

@James Gallicchio can you explain why it is essential in its current form?

[Arthur Paulino]

Example: when you're programming with side-effects inside some stateful monad, you may forget to do something with a variable that's provided to the function. The linter is a straightforward mitigation of such issue

[Arthur Paulino]

This is a real example: we had a hidden bug that we hadn't seen until this linter came up. We were encoding data from some types into a generic data format. Suppose you have inductive X | x : Nat -> Nat -> X and you want to put those two Nats inside an array like #[.nat a, .nat b]. We simply forgot to add b and the linter flagged that b wasn't being used for anything.

The actual example wasn't so simple, so it was hard to see with the naked eye. But the computer sees everything :eyes:

[Chris Hughes]

I don't think this really applies in mathlib then I guess, unless they're genuinely not used at all even implicitly. We don't have bugs because we prove everything and definitions tend not to be very long anyway.

[Mario Carneiro]

Yes, I recall finding at least 3 issues when we first applied the linter to mathlib. It wasn't only meta stuff, some defs were wrong too

[Mario Carneiro]

also unused haves

[Mario Carneiro]

I think it is a valuable lint, even for mathlib

[Mario Carneiro]

We don't have bugs because we prove everything

This is not really true, I've written about this elsewhere. We don't prove everything either, and what about the theorems themselves? We don't prove that the statements are done correctly so some sanity checking is good

[Chris Hughes]

Mario Carneiro said:

Yes, I recall finding at least 3 issues when we first applied the linter to mathlib. It wasn't only meta stuff, some defs were wrong too

What were the issues?

[Mario Carneiro]

referring to the wrong / a shadowed variable in definitions usually

[Mario Carneiro]

I didn't keep track, I can dig them up

[Chris Hughes]

So the actual a was genuinely unused and not used implicitly?

[Mario Carneiro]

yes

[Mario Carneiro]

if it is used implicitly it will usually not be marked by the linter

[Chris Hughes]

The lean4 linter does trigger for variables used implicitly.

[Chris Hughes]

I'm all for the linter in the case where the variables are not used at all.

[Mario Carneiro]

For most of the issues you flagged above, you should just use leading underscore

[Chris Hughes]

But that makes it less readable. This is important. What do we gain with this linter?

[Mario Carneiro]

I disagree that this conveys no useful information - it says that the variable is intentionally unused

[Mario Carneiro]

once you know what it means it's not particularly hard to read

[Mario Carneiro]

the point of the linter is to have an extra check on unused variables, saying "are you sure you wanted to ignore this variable?"

[Mario Carneiro]

because in a not insignificant fraction of cases this is a symptom of a mistake or bug

[Chris Hughes]

When porting we just use a script to get rid of the errors so I'm not sure we think about if we did want to ignore it

[Mario Carneiro]

I would not use that script until at least glancing over the warnings to make sure that they are what I wanted

[Chris Hughes]

We just don't have time for that when porting. A lot of the time I port without understanding stuff very much. I can't usefully perform this check.

[Mario Carneiro]

but the chances of real issues in ported code is somewhat lower than new code

[Mario Carneiro]

so in this particular case I am more okay than I would normally be with auto-fixing unused variable warnings

[Mario Carneiro]

for a lot of warning classes it defeats the point to auto-fix them without any human intervention

[Mario Carneiro]

(some warning classes like unnecessarySeqFocus can totally be auto-fixed and aren't right now only because of tooling limitations)

[Johan Commelin]

Actually, that one is auto-fixed by ./scripts/fix-lints.py.

[Yaël Dillies]

Repeating this again, I see unusedVariables actively discouraging good style by making us drop the names of variables that show up in the tactic state. And Mario's solution of "just add a leading underscore" makes it feel like we're going against the linter, which is not encouraging.

[Mario Carneiro]

Adding a leading underscore is not going against the linter. If the variable is genuinely unused, then both _ and _x indicate this better than x

[Mario Carneiro]

the goal of the linter is to make it obvious by looking at the source code whether variables are unused

[Mario Carneiro]

as well as to give you an "are you sure?" moment when a variable appears to be unused and it is not clear whether that was intentional

[Eric Wieser]

But _ doesn't mean the variable is unused, it just means it's not referred to by name

[Eric Wieser]

I think considering variables "used" if they appear in the type of the result would resolve pretty much all the cases @Yaël Dillies is annoyed about

[Mario Carneiro]

The mathlib unused arguments linter already works like that. I see it as being mostly complementary to the lean linter

[Eric Wieser]

I'm not sure what you mean; I'm pretty sure it rejects fun x => le_refl _ as a proof of ∀ x, x ≤ x

[Mario Carneiro]

the mathlib linter doesn't

[Mario Carneiro]

the one you get with #lint

[Eric Wieser]

I wasn't aware there were two separate linters here. The lean linter complains

[Eric Wieser]

Are you suggesting we ignore the lean linter errors and only listen to the mathlib ones?

[Mario Carneiro]

I'm not suggesting anything, just observing that there are two linters. One acts on syntax and reports if you did not use the name itself (i.e. changing the binding would not break the proof), while the other reports if the elaborated term did not use an argument (i.e. even if you used the hypothesis in a tactic, that hypothesis did not contribute to the final term and can be removed)

[Eric Wieser]

I think this thread is complaining only about the former

[Kyle Miller]

Hijacking this thread for a moment, I've been meaning to ask about about how to add an unused variables ignore function. With that linked ignore function, it only works in the same module as where the ignore function is defined. Is this because the attribute is builtin? Is there some other way to get the attribute to stick across different modules?

[Mario Carneiro]

It looks like the extension just stubs out saving the tagged declarations to disk:

builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ←
  registerSimplePersistentEnvExtension {
    addEntryFn    := fun _ _ => ()
    addImportedFn := fun _ => ()
  }

cc: @Sebastian Ullrich

[Sebastian Ullrich]

Hm yes that looks wrong

[Chris Hughes]

I'll just point out another problem with this linter, which is that we miss out on noticing genuinely unused variables, because this linter doesn't check for that. For example !4#3986. I'm still in favour of changing this linter to check for genuinely unused variables.

[Mario Carneiro]

the mathlib linter should be catching this?

[Yaël Dillies]

I think it can't because the variable is caught in the induction?

[Mario Carneiro]

that certainly makes the analysis a lot harder

[Eric Wieser]

Is this related to the way induction captures a bunch of unused variables that it didn't in lean 3?

[Yaël Dillies]

Once again, can we please turn down/off this linter? In !4#5810 I now have a bunch of statements that talk about _x.

[Yaël Dillies]

I now think that I never want to check whether a variable introduced in a lambda is actually used or not. Constant functions are nice.

[Yury G. Kudryashov]

Should we make a vote? Because I would vote for not removing the linter.

[Yury G. Kudryashov]

I see nothing wrong in fun _x => c

[Yaël Dillies]

Yury, consider the difference between ∀ x, true and λ x, 0. I don't consider x to be unused in the second case.

[Yaël Dillies]

Yury G. Kudryashov said:

I see nothing wrong in fun _x => c

You end up with _x in a lemma statement!

[Eric Wieser]

I'm more opposed to the fun x hx => hx version where the linter is saying "you have to write the explicit type if you want to keep the nice name"

[Eric Wieser]

I think fun _x => c is a grayer area

[Yury G. Kudryashov]

fun _ => 0 clearly says "I am not going to use this input in the output".

[Yury G. Kudryashov]

What lemma statements are you talking about? I searched for _x in the PR and found nothing.

[Yaël Dillies]

I am about to push the fixes. Give me 5min.

[Mario Carneiro]

Eric Wieser said:

I think fun _x => c is a grayer area

I don't even see what is gray about this, the value is quite clearly unused

[Yaël Dillies]

The problem is that I never wrote fun x => c. I wrote ∫ x, c!

[Eric Wieser]

@Yaël Dillies is complaining that ⨍⁻ x, (0 : ℝ≥0∞) ∂μ has to be written as ⨍⁻ _x, (0 : ℝ≥0∞) ∂μ

[Mario Carneiro]

yeah it looks unused there too

[Mario Carneiro]

I'm not seeing a gray area here

[Eric Wieser]

What's "gray" is whether the second version is nicer to read

[Eric Wieser]

There's no grayness as to whether it's unused

[Yury G. Kudryashov]

Why not just ⨍⁻ _, 0 ∂μ?

[Mario Carneiro]

I think it is valuable information to be able to clearly see that the value is unused as a precursor to applying some theorem about how it's equal to the body times the measure of a set

[Mario Carneiro]

the use of prefix underscore to mean "unused" was not really a convention in lean 3, so I can understand why it is unfamiliar, but the point of the linter is to enforce exactly this convention in lean 4

[Mario Carneiro]

you could say it is another aspect of the "naming convention"

[Mario Carneiro]

I think we should get an option in unusedVariables for the issue Eric is bringing up: the linter could be suppressed when the type is dependent

[Mario Carneiro]

I won't take a stance on whether it should be enabled or not in mathlib

[Henrik Böving]

Just to add another reason in favor of having the linter:

I remember that back when the linter was originally introduced it did actually help to find a few mistakes in Lean compiler code because people had introduced identifiers they wanted to refer to and accidentally referred to others. So it's not only useful as a tool for code style but also for silly bugs actually.

[Yaël Dillies]

I maintain that in mathlib it's just noise:

-- doesn't complain
example : Fintype (Iic b) :=
  Fintype.ofFinset (Finset.Iic b) fun x => by rw [Finset.mem_Iic, mem_Iic]

-- unused variable `x` [linter.unusedVariables]
example : Fintype (Iic b) :=
  Fintype.ofFinset (Finset.Iic b) fun x => Finset.mem_Iic

[Yaël Dillies]

(I didn't even have to look for long to find this example, it happened to me literally now)

[Mario Carneiro]

the linter doesn't always trigger when we would like - I think the intention is for both to warn there

[Eric Wieser]

That one is the one that Mario was in favor of adding an option for, right?

[Mario Carneiro]

yes

[Mario Carneiro]

I think this has something to do with the revert/intro idiom, which is the same reason for the "variables get pulled in by cases" issue

[Yaël Dillies]

Ping here. I really want this linter gone watered down. In #6846:

theorem lt_mem_sets_of_limsSup_lt (h : f.IsBounded (· ≤ ·)) (l : f.limsSup < b) :
    ∀ᶠ a in f, a < b :=
  let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_csInf_lt h l
  -- unused variable `c` [linter.unusedVariables]
  mem_of_superset h fun _a => hcb.trans_le'

I'm literally referring to c in the same line.

[Yaël Dillies]

I'll make my point again: If a variable appears in another variable's type, it should be considered used. Else that encourages stripping off names that are never referred to in the code but still contribute positively to the readability of the infoview.

[Yaël Dillies]

Btw tagging the declaration with @[nolint linter.unusedVariables] gives

linter 'linter.unusedVariables' not found

Same deal with @[nolint unusedVariables].

[Thomas Murrills]

(Orthogonal to the point, but btw, I think you're looking for set_option linter.unusedVariables false in—I think this is because of the "two kinds of linters" deal, with unusedVariables being a core linter, and @[nolint] being applicable only to std ("mathlib") linters. Maybe @[nolint] ought to be expanded to cover core linters too, or at least indicate to the user that they ought to use set_option instead if they pass a core linter's name...)

[Scott Morrison]

@Yaël Dillies, if you could make a Mathlib-free example, and create an issue on the Lean repo, that would be helpful!

[Mario Carneiro]

a similar issue happens when variables are used only in Q(_) annotations. If you look in norm_num or ring for instances of variables like _a or _c that's usually what they are working around

[Mario Carneiro]

MWE:

import Qq
open Qq
example : (a : Q(Nat)) × Q($a = 0) → Q(0 = 0) :=
  fun ⟨x, (h : Q($x = 0))⟩ => q(($h).symm.trans $h) -- unused variable x

example : (a : Q(Nat)) × Q($a = 0) → Q(0 = 0) :=
  fun ⟨x, h⟩ => -- ok
    let h : Q($x = 0) := h
    q(($h).symm.trans $h)

Based on this it might just be an issue in that type ascriptions in patterns are not checked

[Mario Carneiro]

Note that this isn't just an issue of the unusedVariables linter. The linter piggybacks on data collected for many purposes, it's just that the linter is the most obvious indicator that something has gone wrong. For example, if you ctrl-click on the x in let h : Q($x = 0) := h it jumps to the x binder, but it fails if you click on the x in (h : Q($x = 0))

[Mario Carneiro]

in fact the exact same example works without Qq:

example : {a : Nat // a = 0} → 0 = 0 :=
  fun ⟨x, (h : x = 0)⟩ => h.symm.trans h -- unused variable x

example : {a : Nat // a = 0} → 0 = 0 :=
  fun ⟨x, h⟩ => -- ok
    let h : x = 0 := h
    h.symm.trans h