experiment for #188 and #429 -- insert show after error in silent mode

[hendriktews]

This is my first partial take on issue #188 and Pierre's example in PR #429 This PR reliably inserts a show command after an error. The following points still need to be solved:

• keep the error message visible and only update the goals buffer in the background
• only insert this show command when the error is hit in silent mode or when the previous command was just unset silent.

This can be done, but would require some new features and additional state in delayed goals/response processing (proof-shell-handle-delayed-output). However, I would question if this makes sense, because I don't see an advantage when running silent. For my biggest files, which take about 11 seconds to process interactively (≈3000 lines), the speedup of silent processing is less then 5%, just a fraction of a second.

[hendriktews]

See #468 for measuring the difference between silent and non-silent processing.

[hendriktews]

@Matafou @cpitclaudel Do you have an opinion here? Shall we make delayed response/goal processing more complicated or simply switch to non-silent?

[cpitclaudel]

I will have a look very soon. Thanks for working on this.

[Matafou]

Thanks Hendriks!

My experiments on the silent stuff date back to more than a decade, maybe two. It was mostly dependent on the size of goals (times the number of tactics processed). Do your tests use big goals (say one page long)? The fact that coq was displaying the goal after each tactic was a serious bottleneck when goals were big. But again this was in the 2000's I think, so maybe this is negligible now.

Other protocols have all switched to silent mode: never show goals unless a "Show" is issued by the ide. It seems the most reasonable to me.

[cpitclaudel]

Concretely, what does silent processing do now that goal printing isn't automatic anymore?

[hendriktews]

@Matafou: Maybe my goals are not so long. In one of the tested files I see about 1400 goals printed, maximum size 88 lines, average 41, and about 700 goals more than 41 lines. Do you have a big file with longer goals?

@cpitclaudel: I am not sure I understand your question. Silent processing issues Set Silent and Unset Silent commands. Without this (eg, with setting full-annotation), all goals are fully printed in the *coq* buffer.

[cpitclaudel]

@cpitclaudel: I am not sure I understand your question.

I thought recent Coq versions printed a lot less when processing, but it seems I was wrong about this.

[Matafou]

@cpitclaudel what you guessed is not true currently, but I think we wan tto switch to it (unless async comes to maturity meanwhile).

@hendriktews

• keep the error message visible and only update the goals buffer in the background

... without triggering your Show again. I remember having a hard time with this one. This is where pg generic mechanism makes things a bit difficult.

• only insert this show command when the error is hit in silent mode or when the previous command was just unset silent.

...and we are inside a proof.

[hendriktews]

The approach of this PR is to submit a Show command after the error to update the goals buffer while keeping the error message somehow visible.

A completely different approach would be to remember the last successful command and, in case of an error, retract to before that command and execute the last successful and the failing command again (of course not silent). I have the impression that this alternative approach would be simpler. Or do I oversee something?

[Matafou]

If the last successful command takes long this may feel frustrating.

[hendriktews]

If the last successful command takes long this may feel frustrating.

Maybe, but note that this does not happen during interactive development, because there you are asserting single commands and do not switch to silent. Do you have a lot of long running commands? And what does long mean?

[Matafou]

It is quite common to have a single command taking several seconds. P.

Le lun. 13 avr. 2020 à 14:39, hendriktews [email protected] a écrit :

If the last successful command takes long this may feel frustrating.

Maybe, but note that this does not happen during interactive development, because there you are asserting single commands and do not switch to silent. Do you have a lot of long running commands? And what does long mean?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/pull/467#issuecomment-612881597, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFSL2QSX4ICBVLPRSKTDYDRMMBXFANCNFSM4LGJJVRA .

[Matafou]

Actually it is generally more frequent during proof development, while e.g. type classes have not yet been fine tuned for your purpose.

[hendriktews]

@Matafou : I would like to repeat to ensure I understand: When fine tuning type classes, you assert bigger chunks (so Coq is switch to silent), in these chunks one command is likely to fail and the command before the failing one takes several seconds to process. Right?

[Matafou]

@Matafou : I would like to repeat to ensure I understand: When fine tuning type classes, you assert bigger chunks (so Coq is switch to silent), in these chunks one command is likely to fail and the command before the failing one takes several seconds to process. Right?

Yes. Actually even after fine tuning type classes some single commands still take a long time to process.

[Matafou]

• keep the error message visible and only update the goals buffer in the background

Maybe the simplest is to store the error message and re-insert it afterward?

• only insert this show command when the error is hit in silent mode or when the previous command was just unset silent.

Maybe this is not so important: issuing a superfluous Show is probably not a problem?

[Matafou]

@hendriktews I am playing with your version and it seems to work quite well.

This is my first partial take on issue #188 and Pierre's example in PR #429 This PR reliably inserts a show command after an error. The following points still need to be solved:

• keep the error message visible and only update the goals buffer in the background

At first glance this seems to work already, doesn't it?

• only insert this show command when the error is hit in silent mode or when the previous command was just unset silent.

This is not so important: making one spurious Show is OK imho if it does not reset the response buffer.

Actually it is the occasion to add a few other missing "Show": Currently when pg has a bunch of commands to process it Set Silent, plays all commands except the last one, then unset silent, then plays the last command. This is not accurate: sometimes the last command is "Proof", or a comment, and the goal is not displayed. What we should really do is set silent, play everything, if the last prompt says there is still a goal, do Show (without reseting response buffer).

[hendriktews]

Hi,

From the discussion in the PR I conclude that my suggestions for running non-silent or to backtrack on error do not get much support. If you prefer the approach of this PR, this is also fine with me.

Pierre Courtieu [email protected] writes:

@hendriktews I am playing with your version and it seems to work quite well.

OK, I deleted the "do not merge" in the PR title.

• keep the error message visible and only update the goals buffer in the background

At first glance this seems to work already, doesn't it?

• only insert this show command when the error is hit in silent mode or when the previous command was just unset silent.

This is not so important: making one spurious Show is OK imho if it does not reset the response buffer.

Then let's postpone these points.

If you want to build on the changes here, then please merge or add other commits to this PR. With proof-add-to-priority-queue you can add stuff to the front of proof-action-list. In cases where proof-action-list is cleared (eg., because of an error) you can also use proof-add-to-priority-queue to generally add stuff to proof-action-list. What we currently don't have, is a function that permits to add stuff at the end of proof-action-list when you are inside the process filter. proof-add-to-queue does this, but I believe it does not work at certain points inside the process filter.

Instead of participating here, I would devote my time on polishing the prooftree support.

Hendrik

[Matafou]

OK I will try to make something from your PR. I never did this before, do I just push directly on your branch?

[erikmd]

@Matafou

OK I will try to make something from your PR. I never did this before, do I just push directly on your branch?

Yes, you can just add hendrik's repo as another remote:

git remote add hendrik [email protected]:hendriktews/PG.git
git fetch hendrik

and checkout/push as usually:

git checkout -b pr-467 -t hendrik/issue-188-pr-429

(given GitHub knows this branch from hendrik is a "PR source branch", you will automatically have write rights for this remote branch)

[Matafou]

OK thanks. Currently your branch falls into a loop if an error occurs when not in a proof (Show sends an error which triggers the same piece of code again, which sends another Show, etc). I know how to fix this, but now I realize that what you implemented is roughly the same as what proof-shell-empty-action-list-command has been made for: https://github.com/ProofGeneral/PG/blob/ea62543527e6c0fcca8bbb70695e25c2f5d89614/generic/proof-shell.el#L1138 So maybe we should adapt this part instead. Still studying things.

[Matafou]

This should work correctly now.

• I had to first commit https://github.com/ProofGeneral/PG/commit/5807535598911346f09db0091ccbb2d1c3283433 to have the information about being in proof mode at this point of the code.
• There are still cases where the goal is not displayed: If a bunch of commands sent to the prover ends with a comment or Proof., no goal is printed since only this (silent) span is processed with Silent Off. To fix this correctly I need to figure out how to detect that no goal were displayed since the beginning of the bunch. Or maybe just check the goal buffer is empty?

[Matafou]

• To fix this correctly I need to figure out how to detect that no goal were displayed since the beginning of the bunch. Or maybe just check the goal buffer is empty?

Or wait for our switch to "always silent, always ask for Show", where we will always send a Show after a command in proof mode.

[Matafou]

by the way @erikmd @CyrilAnac my previous force-push had a spurious debug message left in the code and it made the CI test fail apparently, which is fine, but when going to the log page (https://github.com/ProofGeneral/PG/runs/714045321?check_suite_focus=true) I had a serious bug in my browser due (I guess) to a very long log. This made the diagnostic a bit painful. Do you think this fixable?

[erikmd]

@Matafou

I had a serious bug in my browser due (I guess) to a very long log.

I can't see the log either (I only see This file has been truncated. […] and it seems the CI job lasted during 6h :) so maybe the simplest solution is:

• you disable the debugging feature that is very verbose and re-force-push
• or you run the following command locally to have the full log: cd .../PG/ci && ./test.sh
  (this doesn't require having docker installed)

[Matafou]

I forced pushed a commit and it solved the problem, if I have time I will try to understand why the test took so long. It cannot be just because of the message (one word), can it?

[erikmd]

It cannot be just because of the message (one word), can it?

maybe the issue was some kind of infinite loop (which would explain the 6h+ build time?) adding zillions of copies of the word at stake? but I didn't have a look on the code you mention so I don't know exactly

[erikmd]

In any case, if you note somewhere the SHA1 of the commit at stake, we'll be able to try reproducing the issue with the ./ci/test.sh script locally

[Matafou]

I will. But I think I know the problem. There was indeed a loop in some cases in Hendrik's first try, and my force push did not fix it yet.