premature "goals accomplished"

Stream: mathlib4

[David Renshaw]

Could we report an error (or warning) on the exact line?

[David Renshaw]

It seems to me that the core problem is that the parsing error shows up far away from where it needs to be addressed.

[Heather Macbeth]

Mario and I just PM'd a bit about this, and I quote some of his comments with his permission. He clarifies the proposal from the meeting on Thursday and points out that it still doesn't make "goals accomplished" work as expected in some cases:

the proposal was basically to not use goals accomplished if there are any synthetic sorries in the goal, such as might be created by an erroring tactic

that's still a bit non-local though, for example here:

example : True := by
  have : True := by
    apply id
    exact trivial
    -- here
  apply id
  exact syntax error

in this example, we will get a "goals accomplished" message at the indicated location currently, do you find this to be a good thing or a bad thing? Under the proposal this will be shown as "no goals" because of the syntax error on a later line

[Heather Macbeth]

And regarding the example at hand in this thread, he concludes as @David Renshaw did that the premature "goals accomplished" is really a symptom, not a cause, the cause being Lean 4's "better" (i.e., more optimistic, and less dependent on separators like ,) parser than Lean 3.

that's because lean 3 completely falls over when there is a parse error

when there are parse errors you can't get anything useful from the goal view

so you have to be really good about putting commas and underscores when working with lean

count all the instances of don't forget the comma in NNG

[Heather Macbeth]

Personally, I have come to the conclusion that there is no possibility of having a sensible "goals accomplished" in Lean 4. It is a tradeoff, basically, and we lost it when we got rid of the commas. I propose that we rename "goals accomplished" to "no goals" so that it seems to imply no particular promise.

[Heather Macbeth]

For teaching I would combine that with @Adam Topaz's suggestion of inserting done at the end of each exercise so that at least the errors get localised to one exercise and don't drift into the next. (Or maybe we can bring back begin/end for teaching purposes only.)

[Notification Bot]

8 messages were moved here from #new members > behaviour of exact in lean4 by Heather Macbeth.

[Eric Wieser]

Is wrapping exercises in section/end enough to contain errors?

[Heather Macbeth]

It is, but that's less readable than having begin/end proof blocks in my opinion.

[Adam Topaz]

I imagine it would be quite easy to write a done? variant of done that displays goals accomplished if there are no metavariables and a proof incomplete or something otherwise

[Adam Topaz]

And if we change the generic goals accomished message to "no goals", that would be a reasonable solution IMO

[Heather Macbeth]

Perhaps it doesn't even need to be a variant, this could just be the standard behaviour of done.

[Heather Macbeth]

Or maybe we can call it qed (à la Coq) rather than done?. With unicode □ even!

[Mario Carneiro]

I would rather have us fix our broken heuristics (if we can figure out the behavior we want) than regress the user experience

[Mario Carneiro]

for example, if the issue is that exact reports a parse error on the next command, well let's fix that

[Mario Carneiro]

...where should it report an error?

[Mario Carneiro]

the parser's behavior here is very sensible, it is giving an error on the token that can't be parsed

[Mario Carneiro]

which happens to be the one on the next command

[Adam Topaz]

I agree Mario, of course. But having such a qed tactic would be nice anyway, especially if it gives you a count of the remaining goals.

[Mario Carneiro]

now if that token happens to be to the left of the position mark, then it couldn't be part of the command anyway so maybe we should shift the blame earlier

[Heather Macbeth]

@Mario Carneiro To clarify, which of these proposals do you consider a regression of the user experience? The phrasing "goals accomplished" vs "no goals", or inserting done/qed so that errors don't flow on to the next declaration?

[Mario Carneiro]

the loss of "goals accomplished" in common scenarios is a regression

[Heather Macbeth]

Mario, I thought you didn't care about whether it was called "goals accomplished" or "no goals"?

[Mario Carneiro]

I don't, personally, but some others do and I remember it being a big thing when it was first added to lean 3

[Mario Carneiro]

it's literally just some text but it helps with gamifying the experience

[Mario Carneiro]

inserting done is a fine hack if it helps you with controlling the messages, but it's clearly not where we are going long term

[Mario Carneiro]

and for me personally, I don't like having to add things like that and then remove them when the proof is done, it makes me think about whether it is worth adding in this case and that's a waste of brain cells

[Heather Macbeth]

I'd be delighted if we can get "goals accomplished" working eventually, but in the short term (until someone has time for that) I think renaming to "no goals" is a strict improvement.

[Mario Carneiro]

well I'm trying to evince a specification with these questions

[Mario Carneiro]

I think there is not much preventing us from implementing whatever in this space

[Mario Carneiro]

the server knows a lot about what is going on

[Heather Macbeth]

For such a specification, maybe @Matthew Ballard has some good test cases from his experience teaching with Lean 4.

[Heather Macbeth]

Mario Carneiro said:

now if that token happens to be to the left of the position mark, then it couldn't be part of the command anyway so maybe we should shift the blame earlier

And certainly this seems like an excellent proposed change to exact.

[Patrick Massot]

To be honest I see disparition of begin/end as a big regression whatever the context (teaching or not). Having the error message saying the proof isn't finished at the beginning of the proof is really annoying. I wanted to propose that we simply restore begin/end in mathlib.

[Patrick Massot]

I simply don't understand what is the expected gain in this change. Is it the number of keystrokes? You can easily setup a 2 letters long abbreviation that VSCode turns into begin/end

[Mario Carneiro]

having had a recent need to use pascal, I can say I am really not a fan of begin/end: it is verbose, it doesn't work with bracket matching, it makes indentation around it more work unless you have a good autoformatter

[Sebastian Ullrich]

Heather Macbeth said:

the premature "goals accomplished" is really a symptom, not a cause, the cause being Lean 4's "better" (i.e., more optimistic, and less dependent on separators like ,) parser than Lean 3.

But that would be trivial to at least take into account in the error message - something like "no goals left at this point, but errors are present in the current declaration"

[Jireh Loreaux]

Personally, I could see using done always as a default for teaching. begin ... end just becomes by ... done. For students I think this is ideal because it forces them to claim the proof is over. Maybe there could even be an option to make it a requirement (by Lean) of some sort. Although I'm fine if done were omitted in mathlib.

[Mario Carneiro]

It's easy to make a linter that requires done on all by blocks

[Heather Macbeth]

@Sebastian Ullrich Sure, I even think "no goals" is a suggestive enough message here, and my proposal (at least for the short term) is to rephrase "goals accomplished" to "no goals".

But as Mario points out, a lot of people like the more optimistic "goals accomplished" phrasing if we can find a way to show that when it happens to be appropriate.

[Sebastian Ullrich]

So to clarify, my proposal is to show that specific message only in the circumstance described by it

[Sebastian Ullrich]

And even then, it probably doesn't have to be shown if all remaining error messages are "unsolved goals"

[Mario Carneiro]

Here are some cases that we might want to take into account:

• Goals accomplished :tada: everything is done
• Goals accomplished, but you used sorry
• No goals remaining, a tactic in this block threw an error
• Goals accomplished, but there is an error elsewhere in the proof (not in this block)
• Subgoals accomplished, but this is a by block nested in another one (which may or may not be complete)

[Jireh Loreaux]

@Mario Carneiro would such a linter force done on a subproof without an explicit by?

[Mario Carneiro]

what does that mean?

[Sebastian Ullrich]

Either should be implementable

[Mario Carneiro]

like example : 1 = 1 := rfl instead of example : 1 = 1 := by rfl; done?

[Jason Rute]

I have a silly question. When by is started, tactics have to be on the same line or on later lines and indented right? If so, can't lean 4 find the last indented line and basically automatically run done there with a nice error message?

[Mario Carneiro]

I think it is difficult to get vscode to highlight a span that isn't in the text

[Jireh Loreaux]

No, like when you generate multiple goals and you focus (or further indent?) one of the goals. Sorry, on mobile so typing Lean is hard.

[Mario Carneiro]

like if you have

example : True := by
  apply id

-- ^ that line

with no indentation on the last line, the span we want to highlight is not addressable by vscode line/col indexing

[Mario Carneiro]

it is probably fine to just put a highlight at column 0 though, or the right column provided there is an indent there

[Mario Carneiro]

vscode will round the position to the nearest addressable location no matter what we do, which isn't a horrible place to put the highlight

[Sebastian Ullrich]

Just to give some more context that may not be obvious: an "unsolved goals" error message actually extends over the entire block, but we tweaked its display so that the squigglies are shown on the first line only, as otherwise half your screen is red. That's why you can see the message in the "Messages" (not "All Messages") list even if your cursor is not on the squiggly itself.

[Sebastian Ullrich]

Huh. What though if we put the full line range of the unsolved goals error in the progress bar thingy to the left of the editor?

[Mario Carneiro]

what progress bar?

[Sebastian Ullrich]

The usually-orange progress indicator

[Mario Carneiro]

would it just highlight the error span of the currently displayed message?

[Mario Carneiro]

I think that those kind of messages are generally bugs

[Mario Carneiro]

so I don't want to encourage their use

[Mario Carneiro]

the single line highlighting is a hack to minimize the pain of an error that covers 30 lines, but it should just have a better span

[Sebastian Ullrich]

I would say all error messages should leave a red mark in the progress indicator. I think Isabelle does this as well.

[Mario Carneiro]

you already get red marks from the diagnostics

[Mario Carneiro]

the scroll bar gets little red ticks in it

[Sebastian Ullrich]

You mean on the scroll bar?

[Sebastian Ullrich]

Right, that's helpful too, but if we want to highlight multiple lines as close to the actual editor as possible without swimming in squigglies, the progress indicator seems to be the best choice

[Mario Carneiro]

I don't disagree, I think that would be a good way to handle such errors... but also we should find and remove those errors when we can

[Sebastian Ullrich]

I'm not sure what you mean by that. I'm assuming you don't want to get rid of all "unsolved goals" errors.

[Mario Carneiro]

I think we need to put unsolved goals errors in the right place. As pointed out up-thread they should not be at the by in the first place

[Mario Carneiro]

I really wish we would move forward with empty blocks already, since in that case you could just use . as an alternative to done

[Sebastian Ullrich]

I don't mind empty blocks, but putting . sounds like just another workaround. Especially since there's not all that much space to put squigglies on there.

[Sebastian Ullrich]

In any case, both our proposals don't address the "parse error in exact" issue because there's no "unsolved goals" error there to begin with

[Mario Carneiro]

actually you're right, . isn't good. What should really work is Jason's suggestion, that is simply indenting to the right place

[Mario Carneiro]

because that is invariably where you end up when you are thinking about what to do next

[Mario Carneiro]

I just now ran into this issue with the following pattern:

example : 1 + 1 = 2 ∧ 2 + 2 = 4 := by
  constructor
  ·
  --^ cursor here, 2 + 2 = 4 is displayed as the tactic state

[Trebor Huang]

The rulers in VSCode do appear out of nowhere right? Like, a straight line at the 80th character. Would a similar technique allow the plugin to display something without the presence of text?

[Jon Eugster]

Sebastian Ullrich said:

But that would be trivial to at least take into account in the error message - something like "no goals left at this point, but errors are present in the current declaration"

I think that would be a really good, trivial improvement: use "goals accomplished :tada:" for no goals + no errors, and "no goals" otherwise. At the moment, @Alexander Bentkamp & I are doing exactly that for our in-development Lean4-game.

"unsolved goals" is another issue, but I don't have a perfect suggestion for that... We're currently using a hidden done at the end and then modify when the message is actually displayed.

[Heather Macbeth]

I'd like to record some takeaways from this discussion in core-Lean issues, but since I'm not very experienced here I would first like to check that my summaries are correct.

Firstly, I gather the experts (@Sebastian Ullrich , @Mario Carneiro , ...) think that sometimes what a user experiences as a "premature goals accomplished" is actually a particular tactic behaving badly: it's not throwing an error soon enough, in a situation where it is already clear that there is no valid completion. And in those cases, the tactic should be fixed. For instance, in Damiano's example

example (p : Prop) : p := by
  exact

both Mario and Sebastian apparently diagnose the problem as exact behaving badly: if an unfinished exact is followed by a de-indentation, then report the associated error on exact itself and not the de-indentation. Is that correct, and if so can I open an issue for it?

[Mario Carneiro]

A small amendment: it's not actually exact's job to handle this. The fix would be in the core parser infrastructure / somewhere around the withPosition parser combinator, and so it would affect all parsers using position handling similarly.

[Heather Macbeth]

OK, so in fact it would deal with the same problem for a number of different tactics? That seems even better.

[Heather Macbeth]

So is there a reason that isn't already the behaviour?

[Heather Macbeth]

And another question: Would this also solve the problem that if you have an incomplete proof, the associated red underline shows up at the beginning of the next declaration?

example (p : Prop) : p := by
  not_a_tactic

example (p : Prop) : p := sorry -- error on this line

[Mario Carneiro]

Heather Macbeth said:

So is there a reason that isn't already the behaviour?

The current behavior is also fairly natural: report an error on the first token that is invalid given what the current parser expects. So if you write fun x ?? e then you get an error on ?? because that's not what you are supposed to write there, and the error message will say to try => instead. For withPosition it's a similar story: if you write a token which is too far to the left it's basically the same as the ?? token in this example: we were expecting a not-too-far-to-the-left token and you didn't give me one.

[Mario Carneiro]

Heather Macbeth said:

And another question: Would this also solve the problem that if you have an incomplete proof, the associated red underline shows up at the beginning of the next declaration?

yes

[Mario Carneiro]

well, it depends on the situation

[Mario Carneiro]

but if it's a by block and the example is not indented then yes

[Heather Macbeth]

Then, there is the proposal that we say something weaker than "goals accomplished" (maybe "no goals") under certain circumstances. For example, Mario's proposal that this be done

if there are any synthetic sorries in the goal, such as might be created by an erroring tactic

or @Jon Eugster's proposal that this be done if there are no goals but also some error. I can't tell if these are exactly the same proposal, or if they're slightly different.

[Mario Carneiro]

they are slightly different (and Jon's suggestion is probably better). A synthetic sorry means something probably went wrong (they should only be generated if an error message is produced), but an error message does not have to come with a sorry, and also you can have a failing tactic that does not contribute to the goal and hence leaves no sorry. I think one way to detect errors directly would be to look at the messages list and see if a red squiggle message was emitted

[Heather Macbeth]

I opened
https://github.com/leanprover/lean4/issues/1970
https://github.com/leanprover/lean4/issues/1971
with the proposals from this discussion.

[Sebastian Ullrich]

Mario Carneiro said:

A small amendment: it's not actually exact's job to handle this. The fix would be in the core parser infrastructure / somewhere around the withPosition parser combinator, and so it would affect all parsers using position handling similarly.

Attaching this to withPosition looks dubious. First of all,

  exact
id

is (unfortunately?) perfectly valid. Second, there's no inherent reason why

  if

def

shouldn't have its error position improved as well.

[Wojciech Nawrocki]

Sebastian Ullrich said:

Right, that's helpful too, but if we want to highlight multiple lines as close to the actual editor as possible without swimming in squigglies, the progress indicator seems to be the best choice

Btw, Dafny is perhaps what that looks like in the limit of increasing detail (from https://dafny.org/).

[Heather Macbeth]

Heather Macbeth said:

I opened
https://github.com/leanprover/lean4/issues/1970
https://github.com/leanprover/lean4/issues/1971
with the proposals from this discussion.

I still hope that the devs will take up the "premature goals accomplished" issue eventually. Since this looks like it might take a while, I have opened a PR
https://github.com/leanprover/vscode-lean4/pull/277
to rename "goals accomplished :tada:" to "no goals" in the VS Code extension. This is intended as a temporary measure to make the user experience less confusing.