Feature request: Distinguish between "goals accomplished" and "no goals"

[hrmacbeth]

At the moment, the Lean 4 VS Code extension reports "Goals accomplished 🎉" if the goal list is empty. This is copied from the Lean 3 behaviour (https://github.com/leanprover/vscode-lean/pull/114). However, far more often than in Lean 3, the phrase is an inappropriate descriptor of the situation. For example:

example : True := by
  exact h

With the cursor after h, one has two messages displayed, "Goals accomplished" and "unknown identifier 'h'". In Lean 3, there is no "Goals accomplished" message on this example, I guess because the parser is so confused by the unknown identifier 'h' that it does not output any goal list, empty or not.

This has been discussed in the mathlib porting meetings and several times on Zulip https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Marmite/near/302553129 https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/behaviour.20of.20.60exact.60.20in.20lean4 https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/premature.20.22goals.20accomplished.22

Several people have suggested that the "Goals accomplished" message be be limited to a smaller set of situations. The remaining situations, when the goal list is empty but "Goals accomplished" is not appropriate, could display the message "no goals" or no message at all.

Ideally, the criterion for whether to display "Goals accomplished" would depend only on the current block, and not e.g. be affected by other errors outside that block. For example, this could be done by (programmatically) looking for errors, i.e. red squiggles (a suggestion of Jon Eugster).

If the devs don't want to implement this feature, I'd like to propose that "no goals" be the standard wording in VS Code (and "Goals accomplished" could be turned on by an option). Likewise if the devs do want to implement this feature but expect that it will take some time (say more than a couple of weeks).

[hrmacbeth]

If the devs don't want to implement this feature, I'd like to propose that "no goals" be the standard wording in VS Code (and "Goals accomplished" could be turned on by an option). Likewise if the devs do want to implement this feature but expect that it will take some time (say more than a couple of weeks).

This has now been done in the VS Code extension, so the immediate confusion is resolved. It would still be nice to have the more nuanced behaviour if/when the devs get time.

[fpvandoorn]

Related RFCs:

• #4190 asks for No goals to point to errors elsewhere in the proof. #4190 is slightly incompatible with this feature request, because that RFC requests Lean to show No goals even if there is an error in a different branch, while this feature request requests Lean not to do that.
• #4181 asks to no show No Goals with certain errors.

[hrmacbeth]

I'm closing this issue in favour of #4190, which is a more refined proposal addressing this issue.