Opt out of "included section variable is not used" linter

Stream: lean4

[Yaël Dillies]

Consider the following schematic code:

variable {α : Type*} [Foo α] [Bar α]

private def aux := sorry -- needs `Foo α` but not `Bar α`

private theorem aux_pred := sorry -- The important property of `aux`

private def otherAux := sorry -- needs `Bar α` but not `Foo α`

private theorem otherAux_pred := sorry -- The important property of `otherAux`

theorem big_thm := sorry -- uses `aux` and `otherAux`

[Yaël Dillies]

Before the new variable inclusion mechanism, [Bar α] would be excluded from aux and aux_pred, and [Foo α] from otherAux and otherAux_pred, as expected.

[Yaël Dillies]

Now, [Bar α] is excluded from aux but not aux_pred, and [Foo α] from otherAux and not otherAux_pred.

[Yaël Dillies]

This means that I get linter warnings on aux_pred and otherAux_pred. I really really don't care about those warnings because

1. aux and otherAux are auxiliary declarations whose sole purpose is to prove big_thm
2. rearranging the file to make sure [Foo α] is only visible to aux, aux_pred and big_thm and [Bar α] visible to otherAux, otherAux_pred and big_thm would be unnatural, time-taking and bring no benefit

[Yaël Dillies]

Can I ignore the linter? If so, can the error tell me how to, so that I don't have to ask on Zulip or plough through a release note (which didn't contain that information, FWIW)?

[Mario Carneiro]

here's a MWE version of that example:

import Mathlib.Tactic.TypeStar

class Foo (α : Type*)
class Bar (α : Type*)
variable {α : Type*} [Foo α] [Bar α]

axiom mySorry : ∀ {α}, α

-- needs `Foo α` but not `Bar α`
private def aux : ‹Foo α› = ‹Foo α› := mySorry

-- The important property of `aux`
private theorem aux_pred : aux (α := α) = aux := mySorry

-- needs `Bar α` but not `Foo α`
private def otherAux : ‹Bar α› = ‹Bar α› := mySorry

-- The important property of `otherAux`
private theorem otherAux_pred : otherAux (α := α) = otherAux := mySorry

theorem big_thm : α = α :=
  have := aux_pred (α := α)
  have := otherAux_pred (α := α)
  rfl

[Mario Carneiro]

agreed that the message

included section variable '[Bar α]' is not used in '_private.Mathlib.Test.0.aux_pred', consider excluding it

is poor in a few ways:

• The name _private.Mathlib.Test.0.aux_pred is not properly name-resolved and shows internal details
• The name is not ctrl-clickable to find the declaration
• It's not using the linter framework to show the warning so there is a missing line about using set_option something to disable it

[Mario Carneiro]

cc: @Sebastian Ullrich

[Mario Carneiro]

There is (apparently) no option to specifically disable this warning, but there is the option set_option deprecated.oldSectionVars true which disables the new behavior entirely (i.e. aux_pred will only depend on [Foo α] , not pull in [Bar α] and then complain that it did so)

[Mario Carneiro]

but, well, the name of the option should tell you how much the devs feel like supporting it

[Yaël Dillies]

FWIW I don't really care about reintroducing the old behavior. I think it's perfectly fine having aux_pred and otherAux_pred have unused arguments (again, because they are auxiliary lemmas). I do care about having a warning-less project, however

[Mario Carneiro]

the other option is to use omit [Bar α] in on the lemma in question, but this is both ugly and also seems likely to get a linter warning against it in the near future

[Mario Carneiro]

and unfortunately the converse option include [Bar α] in:

• Doesn't work, you have to include bar and name the variable [bar : Bar α]
• Doesn't suppress the warning, it still complains that you included the variable unnecessarily

[Sebastian Ullrich]

@Yaël Dillies Thanks, that's a sensible use case for disabling the warning. lean#5036

[Yaël Dillies]

:tada:

[Stephan Maier]

Sebastian Ullrich said:

Yaël Dillies Thanks, that's a sensible use case for disabling the warning. lean#5036

Thank you. I having the same problems, and I now fear that I, from not on, have to explicitly list all assumptions of a theorem, making the variable-list useless. In fact, the popups in VS Code now list all the unused hypothesis, making my code base rather clumsy, or in fact, unusable. That, behaviour, I hope, is not intended as it would vastly complicate writing readable code. Do you have any idea what will happen?
Cheer, Stephan

[Stephan Maier]

Sebastian Ullrich said:

Yaël Dillies Thanks, that's a sensible use case for disabling the warning. lean#5036

Hi, thanks for the hint. I just edited the lake-file and now we are back to normal behaviour, including the popus in VS Code:

package "greenhouse" where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`deprecated.oldSectionVars, true⟩
  ]

[Sebastian Ullrich]

Do you have a representative example? Note that the new behavior has been designed in concert with a (successful) adjustment of Mathlib to it so it is not exactly unusable there.

[Stephan Maier]

Sebastian Ullrich said:

Do you have a representative example? Note that the new behavior has been designed in concert with a (successful) adjustment of Mathlib to it so it is not exactly unusable there.

Yes, I hope this compiles:

-- The variables
variable {𝕜 : Type u} [Ring 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜]
variable {V : Type v} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [TopologicalAddGroup V] [ContinuousSMul 𝕜 V]
variable {P : Type w} [AddTorsor V P] [TopologicalSpace P] [htopAddTorsor : TopologicalAddTorsor V P]

-- No trouble with this:
def vector_to (fromP toP: P) : V := toP -ᵥ fromP

-- But here I get the warning: included section variable '[TopologicalAddGroup V]' is not used in
-- 'Affine.vector_to_continuous', consider excluding it
@[continuity] theorem vector_to_continuous (p : P) : Continuous (vector_to p) := by
  let f (q : P) := (q, p)
  have h_comp : (fun pp : P × P => pp.1 -ᵥ pp.2) ∘ f = vector_to p := by
    funext; simp [vector_to]
  rw [← h_comp]
  apply Continuous.comp
  · exact htopAddTorsor.continuous_vsub
  · have h_cont_f : Continuous f := by
      simp [f]; constructor
      exact (ContinuousMap.id P).continuous_toFun
      exact (ContinuousMap.const P p).continuous_toFun
    exact h_cont_f

Also the method-declaration as shon in the popup reads: "Affine.vector_to_continuous.{v, w} {V : Type v} [AddCommGroup V] [TopologicalSpace V] [TopologicalAddGroup V] {P : Type w} [AffineSpace V P] [TopologicalSpace P] [htopAddTorsor : TopologicalAddTorsor V P] (p : P) : Continuous (vector_to p)"

Adding the deprecated.oldSectionVarsas shown above makes this behaviour go away.

[Stephan Maier]

Sebastian Ullrich said:

Do you have a representative example? Note that the new behavior has been designed in concert with a (successful) adjustment of Mathlib to it so it is not exactly unusable there.

I use Lean 4.11 RC2 and have created a new project in VS Code using Mathlib.

[Sebastian Ullrich]

The motivation for the new behavior is documented here: https://github.com/leanprover/lean4/pull/5000/files#diff-724a0c71974c910be02a47643aa12bd62807d6b0565fba65b029d81163ab5500

[Patrick Massot]

Stephan Maier said:

Sebastian Ullrich said:

Do you have a representative example? Note that the new behavior has been designed in concert with a (successful) adjustment of Mathlib to it so it is not exactly unusable there.

Yes, I hope this compiles:

As explained at #mwe, there is a very simple way to check this hope. In the code snippet, click the “go to playground” link in the upper-right corner.

[Patrick Massot]

Hint: your snippet has no import line at all, so the success probability is very low.

[Stephan Maier]

Sebastian Ullrich said:

The motivation for the new behavior is documented here: https://github.com/leanprover/lean4/pull/5000/files#diff-724a0c71974c910be02a47643aa12bd62807d6b0565fba65b029d81163ab5500

Thanks for pointing this out. The rationale is understandable. But we are all lazy and now must change habits... ;-). Not to mention the codebase.
Yours, Stephan

[Michael Rothgang]

@Stephan Maier I tried to fix your example; can you help?

• I needed to add import Mathlib
• then, TopologicalAddTorsor is not defined - can you supply the definition? (I removed that hypothesis and replaced it by sorry, but then your warning does not reproduce.)

import Mathlib
set_option deprecated.oldSectionVars true

variable {𝕜 : Type u} [Ring 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜]
variable {V : Type v} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [TopologicalAddGroup V] [ContinuousSMul 𝕜 V]
variable {P : Type w} [AddTorsor V P] [TopologicalSpace P]

-- No trouble with this:
def vector_to (fromP toP: P) : V := toP -ᵥ fromP

-- But here I get the warning: included section variable '[TopologicalAddGroup V]' is not used in
-- 'Affine.vector_to_continuous', consider excluding it
@[continuity] theorem vector_to_continuous (p : P) : Continuous (vector_to p) := by
  let f (q : P) := (q, p)
  have h_comp : (fun pp : P × P => pp.1 -ᵥ pp.2) ∘ f = vector_to p := by
    funext; simp [vector_to]
  rw [← h_comp]
  apply Continuous.comp
  · sorry
  · have h_cont_f : Continuous f := by
      simp [f]; constructor
      exact (ContinuousMap.id P).continuous_toFun
      exact (ContinuousMap.const P p).continuous_toFun
    exact h_cont_f

[Stephan Maier]

Michael Rothgang said:

Stephan Maier I tried to fix your example; can you help?

• I needed to add import Mathlib
• then, TopologicalAddTorsor is not defined - can you supply the definition? (I removed that hypothesis and replaced it by sorry, but then your warning does not reproduce.)

import Mathlib
set_option deprecated.oldSectionVars true

variable {𝕜 : Type u} [Ring 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜]
variable {V : Type v} [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [TopologicalAddGroup V] [ContinuousSMul 𝕜 V]
variable {P : Type w} [AddTorsor V P] [TopologicalSpace P]

-- No trouble with this:
def vector_to (fromP toP: P) : V := toP -ᵥ fromP

-- But here I get the warning: included section variable '[TopologicalAddGroup V]' is not used in
-- 'Affine.vector_to_continuous', consider excluding it
@[continuity] theorem vector_to_continuous (p : P) : Continuous (vector_to p) := by
  let f (q : P) := (q, p)
  have h_comp : (fun pp : P × P => pp.1 -ᵥ pp.2) ∘ f = vector_to p := by
    funext; simp [vector_to]
  rw [← h_comp]
  apply Continuous.comp
  · sorry
  · have h_cont_f : Continuous f := by
      simp [f]; constructor
      exact (ContinuousMap.id P).continuous_toFun
      exact (ContinuousMap.const P p).continuous_toFun
    exact h_cont_f

Dear Michel

Thanks for helping out! That is kind. I think, I sort out the new approach myself and I will not trouble you. It's easy enough. The lemmas I wish to prove are sometimes just (simple algebraic) calculations, sometimes they need a little topology. I need to move these into separate sections now in order to use variables as (now) intended. This is just tedious but not difficult. And along the way I tidy up other matters, too. In doing Mathlib/Lean so often seems to be going around in cicles, but that is fine ;-)

Thanks once again!
Stephan