Zulip Chat Archive

Stream: mathlib4

Topic: premature "goals accomplished"


David Renshaw (Dec 17 2022 at 13:43):

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

David Renshaw (Dec 17 2022 at 13:44):

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 (Dec 17 2022 at 13:55):

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 (Dec 17 2022 at 13:58):

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 (Dec 17 2022 at 14:02):

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 (Dec 17 2022 at 14:02):

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 (Dec 17 2022 at 14:07):

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

Eric Wieser (Dec 17 2022 at 14:09):

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

Heather Macbeth (Dec 17 2022 at 14:10):

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

Adam Topaz (Dec 17 2022 at 14:11):

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 (Dec 17 2022 at 14:12):

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

Heather Macbeth (Dec 17 2022 at 14:15):

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

Heather Macbeth (Dec 17 2022 at 14:18):

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

Mario Carneiro (Dec 17 2022 at 14:20):

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 (Dec 17 2022 at 14:21):

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

Mario Carneiro (Dec 17 2022 at 14:21):

...where should it report an error?

Mario Carneiro (Dec 17 2022 at 14:22):

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

Mario Carneiro (Dec 17 2022 at 14:22):

which happens to be the one on the next command

Adam Topaz (Dec 17 2022 at 14:22):

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 (Dec 17 2022 at 14:23):

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 (Dec 17 2022 at 14:23):

@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 (Dec 17 2022 at 14:23):

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

Heather Macbeth (Dec 17 2022 at 14:23):

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

Mario Carneiro (Dec 17 2022 at 14:24):

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 (Dec 17 2022 at 14:24):

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

Mario Carneiro (Dec 17 2022 at 14:25):

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 (Dec 17 2022 at 14:27):

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 (Dec 17 2022 at 14:28):

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 (Dec 17 2022 at 14:28):

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

Mario Carneiro (Dec 17 2022 at 14:29):

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

Mario Carneiro (Dec 17 2022 at 14:29):

the server knows a lot about what is going on

Heather Macbeth (Dec 17 2022 at 14:29):

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

Heather Macbeth (Dec 17 2022 at 14:34):

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 (Dec 17 2022 at 14:55):

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 (Dec 17 2022 at 14:57):

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 (Dec 17 2022 at 15:00):

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 (Dec 17 2022 at 15:07):

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 (Dec 17 2022 at 15:07):

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 (Dec 17 2022 at 15:10):

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

Heather Macbeth (Dec 17 2022 at 15:11):

@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 (Dec 17 2022 at 15:14):

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

Sebastian Ullrich (Dec 17 2022 at 15:15):

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

Mario Carneiro (Dec 17 2022 at 15:16):

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 (Dec 17 2022 at 15:16):

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

Mario Carneiro (Dec 17 2022 at 15:17):

what does that mean?

Sebastian Ullrich (Dec 17 2022 at 15:17):

Either should be implementable

Mario Carneiro (Dec 17 2022 at 15:17):

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

Jason Rute (Dec 17 2022 at 15:17):

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 (Dec 17 2022 at 15:18):

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

Jireh Loreaux (Dec 17 2022 at 15:18):

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 (Dec 17 2022 at 15:19):

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 (Dec 17 2022 at 15:21):

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 (Dec 17 2022 at 15:22):

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 (Dec 17 2022 at 15:22):

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 (Dec 17 2022 at 15:23):

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 (Dec 17 2022 at 15:23):

what progress bar?

Sebastian Ullrich (Dec 17 2022 at 15:24):

The usually-orange progress indicator

Mario Carneiro (Dec 17 2022 at 15:25):

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

Mario Carneiro (Dec 17 2022 at 15:25):

I think that those kind of messages are generally bugs

Mario Carneiro (Dec 17 2022 at 15:25):

so I don't want to encourage their use

Mario Carneiro (Dec 17 2022 at 15:26):

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 (Dec 17 2022 at 15:26):

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

Mario Carneiro (Dec 17 2022 at 15:27):

you already get red marks from the diagnostics

Mario Carneiro (Dec 17 2022 at 15:27):

the scroll bar gets little red ticks in it

Sebastian Ullrich (Dec 17 2022 at 15:27):

You mean on the scroll bar?

Sebastian Ullrich (Dec 17 2022 at 15:29):

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 (Dec 17 2022 at 15:32):

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 (Dec 17 2022 at 15:33):

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 (Dec 17 2022 at 15:35):

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 (Dec 17 2022 at 15:36):

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 (Dec 17 2022 at 15:39):

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 (Dec 17 2022 at 15:40):

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 (Dec 17 2022 at 15:47):

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 (Dec 17 2022 at 15:47):

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

Mario Carneiro (Dec 17 2022 at 15:49):

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 (Dec 17 2022 at 18:17):

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 (Dec 18 2022 at 00:55):

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 (Dec 19 2022 at 02:14):

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 (Dec 19 2022 at 02:18):

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 (Dec 19 2022 at 02:18):

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

Heather Macbeth (Dec 19 2022 at 02:19):

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

Heather Macbeth (Dec 19 2022 at 02:21):

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 (Dec 19 2022 at 02:22):

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 (Dec 19 2022 at 02:23):

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 (Dec 19 2022 at 02:23):

well, it depends on the situation

Mario Carneiro (Dec 19 2022 at 02:24):

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

Heather Macbeth (Dec 19 2022 at 02:29):

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 (Dec 19 2022 at 02:48):

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 (Dec 19 2022 at 05:51):

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

Sebastian Ullrich (Dec 19 2022 at 09:20):

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 (Dec 21 2022 at 03:59):

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 (Jan 11 2023 at 00:46):

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.


Last updated: Dec 20 2023 at 11:08 UTC