Disable `linter.unusedTactic` in errored proofs

Stream: mathlib4

[Andrew Yang]

Is it possible to disable linter.unusedTactic and linter.unreachableTactic in proofs with error? When there is an error on some line, every next line gets flagged with linter.unreachableTactic which is unhelpful and quite distracting. The same line also gets flagged by linter.unusedTactic which is just wrong because it did do something: create an error.
A typical example:
image.png

[Aaron Liu]

Probably some set_option

[Andrew Yang]

I would hope this could be done globally. I think remembering a magic spell and casting it whenever you want to fix some proof isn't really user friendly.

[Aaron Liu]

Maybe if you put it in your lakefile

[Yaël Dillies]

This is a v4.19.0 regression FYI

[Aaron Liu]

I think if you have

lean_lib Foo where
  leanOptions := #[
    ...,
    ⟨`linter.unusedTactic, false⟩,
    ⟨`linter.unreachableTactic, false⟩,
    ...
  ]

in your lakefile it will disable it globally

[Aaron Liu]

(not tested)

[Eric Wieser]

Previously the linter would abort early if the proof reported that there was a sorry

[Andrew Yang]

The point is to disable it globally for errored proof only.

[Eric Wieser]

What you ask for is how it always behaved in older versions

[Andrew Yang]

I think lean4#8101 is meant to fix this