unknown tactic

Stream: lean4

[Floris van Doorn]

The code

example : True := by nope

produces the error unknown tactic. How hard would it be to print the error unknown tactic 'nope'?

I had some people using suggest (my alias for library_search) and they got the unknown tactic error. I realize only a few hours later that this error was because the sugges tactic is an unknown tactic, and the suggest tactic was still running.

[Mario Carneiro]

should be easy, the unknown tactic tactic is an ident parser

[Patrick Massot]

I agree that Floris' suggestion will already be a great improvement but it would also be nice to fix the underlying problem that this error message shouldn't stay like this. I noticed this is indeed very confusing.

[Mario Carneiro]

I'm confused what distinction you are making. Floris's suggestion is to improve the error message, no?

[Mario Carneiro]

or do you think the behavior needs to change more radically?

[Floris van Doorn]

Patrick, are you saying that the unknown tactic error message should disappear when suggest is running. I'm not sure if that is good. I definitely want to see the goal view while Lean is running.

[Patrick Massot]

I want to see the goal but not the unknown tactic error

[Kevin Buzzard]

One could imagine that the error is cleared when the next key is pressed. In Lean 3 you used to see weird errors like unknown import data.real.basi which were confusing when in the file you've clearly typed data.real.basic.

[Patrick Massot]

Yes exactly. Here the outdated error stays on display for a very long time because Lean is working on something else.

[Mario Carneiro]

Kevin Buzzard said:

One could imagine that the error is cleared when the next key is pressed. In Lean 3 you used to see weird errors like unknown import data.real.basi which were confusing when in the file you've clearly typed data.real.basic.

This is annoying though because while you are typing you see no information, rather than an unbroken (if delayed) infoview

[Mario Carneiro]

I would much rather have it hold the last message if it has nothing useful to display, possibly with a spinner or something to indicate it is out of date

[Mario Carneiro]

this is especially important if you are typing something based on the goal view (e.g. the type of a hypothesis), since you might forget what it was halfway through typing

[Julian Berman]

Couldn't that be mitigated by various long-running things sending more LSP diagnostics themselves, just not error ones?

[Julian Berman]

E.g. the Processing... LSP info diagnostic messages -- or tactic specific ones saying suggest is searching through lemmas or whatever that gets sent on start and cleared when it's done

[Floris van Doorn]

Mario Carneiro said:

I would much rather have it hold the last message if it has nothing useful to display, possibly with a spinner or something to indicate it is out of date

A visual indication on all outdated message would also be very helpful! With "outdated message" I mean here any message that is produced by a line in the "yellow bar zone" (i.e. that will be recompiled without any additional keystrokes). I think this should include the goal view, assuming the visual indication is not too obtrusive.

[Sebastian Ullrich]

Good point with the yellow bar, that should mean it's implementable in the extension without touching core