unusedHaveSuffices linter in the presence of sorries

Stream: general

[Michael Rothgang]

Suppose I have a lemma whose proof uses sorry: then I would like to silence the unusedHaveSuffices linter. MWE:

import Batteries

theorem foo : True := by
  have : 1 + 1 = 2 := sorry -- Imagine some useful intermediate step.
  -- Imagine a long and complicated proof, which may depend on other sorries.
  sorry

#lint unusedHavesSuffices -- This complains about `this` being unused.

This comes up in large projects, like FLT or Carleson: while the project is ongoing, many lemmas will depend on some sorry. At the same time, having intermediate states as a have can be useful (e.g., to check that an intermediate lemma you wrote actually applies in the setting you want it to). If the proof is not yet complete, such have's may be unused.
I'd argue this is not a useful warning yet: if a lemma is sorry-free, I'd like to see it, but not yet.
Impact. This causes false positives and warning spam when running #lint (or runLinter) in downstream projects like FLT or Carleson. It is one reason I'd not run linters by default. But that means I'm missing out on e.g. the defLemma linter, which is very useful to have.

(There could be other ways to fix this, such as making runLinter more configurable, allowing to enable or disable specific linters. I'd argue that is orthogonal to this change, and both changes should be made.)

[Sebastian Ullrich]

The unused variables linter deactivates itself in the presence of sorries, similar linters should likely all do the same

[Eric Wieser]

I think this is a regression, and previously these did silence themselves?

[Floris van Doorn]

Sebastian Ullrich said:

The unused variables linter deactivates itself in the presence of sorries, similar linters should likely all do the same

A similar thing for errors doesn't work correctly anymore in the current release candidate.

/--
error: unknown identifier 'bar'
---
error: unsolved goals
hf : 1 = 1
⊢ 2 = 2
---
warning: unused variable `hf`
note: this linter can be disabled with `set_option linter.unusedVariables false`
-/
#guard_msgs in
theorem foo (hf : 1 = 1) : 2 = 2 := by
  have := bar
  rfl

[Sebastian Ullrich]

Thanks for the reports, this should be fixed in lean#8101