Add option to consider error message feedbacks as failures (& Fix retract bugs)

[psteckler]

There is an option, settable in coq/coq-system.el, to consider feedbacks with error message as failures, so they cause a retraction to the start of the span associated with the state id in the feedback.

Not well-tested, works on simple examples.

Fixes #232.

[erikmd]

Thanks @psteckler, but this patch doesn't seem to work: with example #232 (comment), both "point 1" and "point 2" cases now trigger some awkward behavior...

[psteckler]

I will try that example.

[psteckler]

With the "retract-on-feedback" option enabled, the behavior for the "point 1" and "point 2" cases is the same.

The error in bug1 causes an error feedback to be issued, with a state id of 4, which is associated with that statement. That causes an immediate retraction, so any feedback that might otherwise be issued for bug2, if you did a goto-point for "point 2", does not get sent.

You don't want to retract to state 4, because that's the state after bug1 has been added succesfully. Coq sends a good-value with that state id, and PG/xml associates bug1 with 4. You want to be able to fix the error, then re-send the statement.

So instead, PG/xml sets the point to the start of the span for bug1, and retract to that point. The actual Edit_at that's sent contains state id 3.

The false in bug1 gets highlighted in red when the retraction occurs, because that's where the error is. Upon the retraction, the point is supposed to be set to the start of the error. There was a bug that prevented that, I have a fix soon to be committed.

[psteckler]

With the latest commit, in the example, the point should be at the start of the marked-in-red "false".

There's also some other cleanup.

[erikmd]

Thanks @psteckler! I'll test this tomorrow.

[erikmd]

Hi @psteckler!
I've tested your commit 543ce8d with option coq-errormsg-as-failure either set or unset, and here is some feedback:
with (setq coq-errormsg-as-failure t) it works like a charm 👍

However with (setq coq-errormsg-as-failure nil) I observe some buggy behavior that did not show up with current version of async branch. So I guess your patch should be refined for that case...

I'm attaching a video that describes the 3 bugs that show up with 543ce8d and (setq coq-errormsg-as-failure nil) (1 bug corresponds to goto-point 2 just after the final dot of the Coq phrase; the 2 other bugs correspond to goto-point 1): video_bugs_pg_async_commit_543ce8d.mkv.gz

Hopefully you can take a look on this afternoon.
Kind regards,
Erik

Edit: the file being used in the video is

(*
  GNU Emacs 25.1.1 under GNU/Linux with
  PG commit 543ce8d67e6f53f15b7475463fba9a975ed315d9
  Coq version 8.7.2
  OCaml version 4.06.1
  (setq coq-errormsg-as-failure nil)
 *)

Definition f (n : nat) := n. (* first, evaluate this line *)

Definition bug1 := f false. (* point 1 *)

Definition bug2 := f false. (* point 2 *)

[erikmd]

@psteckler
To elaborate on the case when coq-errormsg-as-failure = nil I'd say the expected behavior is as follows:

• if we goto-point 1 (only one Coq phrase is processed):
  • if there is only an error message (no failure): goto-point 1 with no retraction
  • if there is a failure (like in my example): it is fine to retract the span to the end of the last succeeding proof command, but I'd strongly prefer that the point is retracted to the beginning of the failure. This way, it would behave like pg: proof-shell did and it would fully solve Upon error, PG/xml stops at the end of the last succeeding proof command? #232, even in the case when coq-errormsg-as-failure = nil.
• if we goto-point 2: apart from the bug I reported (a failure is considered as a bare error-message), the current behavior is OK

[psteckler]

@erikmd I made some "optimizations" to the handle-failure case that were just plain wrong, explaining the change in behavior.

I've fixed that (not yet pushed), and in the goto-point-1 case, the failure causes a retraction to the preceding statement, and the point is at the beginning of the false. I think that's your desired behavior.

The goto-point-2 case differs between Coq master and 8.5.

With 8.5, adding the two buggy statements succeed, but there's a fail-value when we ask for the current goal. That fail-value has a valid state id corresponding to the first statement, the Definition. Before that fail-value arrives, there have been two error feedbacks, which color both falses. After the retraction, the point is on the second false, not the first one. PG/xml uses a heuristic, when a fail-value is returned, to find the error in the span of the last statement added. In fact, that fail-value does correspond to that statement, even though we don't get the fail-value until we ask for a goal. I think this is acceptable behavior.

With master, again we get the two error feedbacks, and we also get a fail-value when asking for the goal. But this time, the fail-value has a dummy state id (a Coq bug, I think), so we don't know where to retract to. I have an idea on how to handle this, which I'm working on now.

[erikmd]

@psteckler

I've fixed that (not yet pushed), and in the goto-point-1 case, the failure causes a retraction to the preceding statement, and the point is at the beginning of the false. I think that's your desired behavior.

Indeed, thanks 👍

[erikmd]

BTW did you reproduce the other bug I mentioned in the video with Coq 8.7.2 ?
namely when we type C-c C-RET exactly after the final dot (but not after a comment or so), there is an error-message instead of a failure?
Indeed IINM, this very last issue is different from the one you describe with Coq master ?
Edit: and it seems to concern both goto-point-1 and goto-point-2 cases.

[psteckler]

I've just pushed a commit, so that if a fail-value has a dummy state id, we look up the state id associated with the span for the last statement added. That is, we try to retract exactly one statement.

For the goto-point-2 case with master, the result is a cascade of retracts back to the Definition. The end result is, 8.5 and master end up the same, with the point on the second false.

[psteckler]

namely when we type C-c C-RET exactly after the final dot (but not after a comment or so), there is an error-message instead of a failure?

I will look at this now.

[psteckler]

With 8.7.2 and master, I am seeing a fail-value when I do C-c C-RET with the point just after the dot for the second statement, or the third statement. That's with the code I just pushed.

[erikmd]

@psteckler, it is indeed a fail-value (I believed it was a bare error-message because it was yellow for a bit longer than usually, but in the end the error indeed becomes red, as expected)

[erikmd]

@psteckler Sorry I'm a bit confused as I did another test with the latest version of the PR (a252075), and it seems that the goto-point-2 behavior has changed: when coq-errormsg-as-failure = nil and I want to process the whole file, it retracts at the last error? is it the expected behavior?

[psteckler]

it retract at the last error? is it the expected behavior?

Yes, with master or 8.7.2, there's a retract to the previous statement, which triggers another retract to the Definition statement.

Before my change, the fail-value with a dummy state id did not cause a retraction. I'm pretty sure that's a Coq bug: a fail-value should tell you what the last valid state id is. The current behavior works around that bug, and gives the same result as 8.5.

[erikmd]

Sorry but I'm not sure I follow you. Even if there is a fail-value, in "goto-point-2" mode, isn't PG supposed to process all the phrases and not retract ?
because up to now retraction (with Coq 8.5, 6.7, 8.7) was only triggered in "goto-point-1" mode, to the first fail-value. But now with Coq 8.7, it retracts to the last fail-value in all cases, which is maybe not very intuitive...

[erikmd]

To be more precise: i think the "goto-point-1" mode (when one evaluates only one Coq phrase) is very fine now and with the option you implemented in this PR it will nicely solve #232.

But IMO the "goto-point-2" behavior we are talking about could be somewhat reverted to that of 543ce8d, because that behavior tested in my video-based bugreport was OK.

[erikmd]

Besides, if we evaluate the small running example file in a row, we now get in the mini-buffer the error message for the first definition, while the cursor is retracted to the second definition:

you can test with

Definition f (n : nat) := n. (* first, evaluate this line *)

Definition bug1 := f true. (* point 1 *)

Definition bug2 := f tt. (* point 2 *)

BTW could you recall what would be the emblematic example of error-message with no fail-value ?

[psteckler]

in "goto-point-2" mode, isn't PG supposed to process all the phrases and not retract ?

PG is simply responding to what Coq sends. For the "goto-point-2" case, there is a fail-value sent by Coq.

If we add an additional statement:

Definition nobug3 := f 42. (* point 3 *)

and goto point 3, there is no fail-value sent, just the error feedbacks. In that case, PG processes nobug3, there's no retraction, though the two falses get marked in red.

[erikmd]

OK I see, thanks for your explanation! :)

[erikmd]

Finally as I mentioned in my last-but-one comment, maybe one improvement could be done to avoid that at the same time, PG retracts to the last error at "point 2" (assuming there is no "point 3") but shows the error message for the first error at "point 1". What do you think?

[psteckler]

you can test with ...

This is a funny one, indeed.

What happens is the cascade of fail-values and retracts I mentioned earlier, which starts with the fail-value containing a dummy state id. The last retract is triggered by a fail-value for bug1, which contains that error message. PG is clearing the *response* buffer when it prints a fail-value error message.

Strangely, with 8.5, where we get a fail-value with a valid state id after processing bug2, that fail-value has the same error message, corresponding to the error in bug1.

In any case, both errors are highlighted, and you can mouse-hover to see the error messages for each one.

[psteckler]

PG retracts to the last error at "point 2" (assuming there is no "point 3") and shows the error message for the first error message "point 1"

With 8.7.2/master, that's exactly what PG attempts. It gets a dummy state id in a fail-value, tries to retract exactly one statement. The result is another fail-value, this time with a valid state id, and does another retraction.

[psteckler]

BTW could you recall what would be the emblematic example of error-message with no fail-value ?

The example with nobug-3 that I showed: there are error feedbacks for bug1 and bug2, and after processing nobug3, and asking for the goal, there's no fail-value.

It seems to depend when PG asks for the goal. If it's immediately after a statement that generates an error feedback, you get a fail-value. If there's an intervening statement that does not generate an error feedback, there's no fail-value. It's that second case that allows for async proof processing in the presence of errors, because you can continue to process statements.

[psteckler]

Note: this is all very confusing! :-)

[erikmd]

In any case, both errors are highlighted, and you can mouse-hover to see the error messages for each one.

Yes: I tested the example and each error indeed has an error-message tooltip, which is very handy. But both error-messages in the tooltips are the same (corresponding to the first error-message) with Coq 8.7.2.
Is it normal, according to what you explained about Coq 8.7.2/master in an earlier comment? Or could this be easily fixable in PG in your opinion?

[erikmd]

But both error-messages in the tooltips are the same (corresponding to the first error-message) with Coq 8.7.2.
Is it normal, according to what you explained about Coq 8.7.2/master in an earlier comment? Or could this be easily fixable in PG in your opinion?

I observe the same little bug with Coq 8.6.1

[erikmd]

Note: this is all very confusing! :-)

Indeed it's a bit tricky :-) but I guess we'll be able to document it somewhere in the wiki for example, so that users feel more familiar with it.

[psteckler]

both error-messages in the tooltips are the same

That's a bug. I'll look into it now.

Is it normal, according to what you explained about Coq 8.7.2/master

I believe that sending a dummy state id in a fail-value is a Coq bug. The code in this PR is doing its best to work around it.

[erikmd]

BTW @psteckler feel free to add a separate commit in this PR if you can fix that remaining bug related to retraction and error messages (we'll be able to squash-and-merge if need be)

[erikmd]

Thanks @psteckler! I just tested the latest version of the PR (e9b61aa) with Coq 8.6.1 and Coq 8.7.2, both with coq-errormsg-as-failure set and unset and it sounds great 👍
So as far as I'm concerned I'm OK to merge this PR in async as is.
If there is no objection I'll do the merge tomorrow Wednesday.
Thanks again Paul :)

[psteckler]

@erikmd actually, I just pushed a fix for that bug.

When PG gets a fail-value, it queues the error message to display later. It was using the span for the last statement sent for that, even though the fail-value error may have come from an earlier statement, as in this case.

With the fix, PG looks at the state id that it's retracting to, and associates the error with the statement that was Added with that state id. That must be the statement that required retracting to that state id.

In this case, we see just the error in bug1 highlighted. I think that's the correct behavior, because that's the error that caused the retraction, and later errors may be invalidated once you fix the retraction-related error. That's not true in this case, of course.

[psteckler]

@erikmd Great, you might want to look again with this latest bug fix, though it should only affect error highlighting.

[erikmd]

@psteckler Yes, this is exactly the version I tested, with your latest bug fix (cf. the SHA1 in my comment) so the tooltips for error highlighting are very OK :-)
Cheers, Erik