Linters on v4.19.0-rc2

Stream: mathlib4

[Christian Merten]

It seems that a few linters behave differently on the new version, e.g.

import Mathlib

theorem foo : True := by
  have : False = _ := by rfl
  rw [this]
  trivial

now shows linter warnings on each of the lines (unreachableTactic and unusedTactic), while there are none on v4.18.0. I think the old behaviour was better, currently I just start all of my files with disabling every linter that get's in my way.
Maybe it has something to do with the new parallel elaboration?

(I even have an example where the unusedVariables linter flags the theorem I am proving as an unused variable, but I did not manage to minimize that one yet.)

[Kevin Buzzard]

Yeah I just ran into this too in FLT and I'm doing the same (it's hard to see the red underlines under the yellow ones so I'm switching all the yellow ones off for my own sanity)

[Bhavik Mehta]

I think lean4#8101 is meant to fix this