Experiments to fix the goals not showing on errors.

[Matafou]

This is in no way a real pull request, just experiments to understand how we could insert a "Show" command after an error occured. It comes from a discussion with @hendriktews.

In its current state the patch "works". But it is certainly not in the right place and needs to be made less adhoc. See comments in the patch.

To reproduce the bug without this patch and see how it is fixed with it, follow these instructions.

Definition eq_one (i:nat) := i = 1.
(* eq_one is delta_reducible but I don't want it to be reduced. *)
Lemma foo: (eq_one 1 -> False) -> False.
Proof.
  (* ask coq to process these two lines together.  *)
  intros H. 
  intro.
  (* without the patch you should see the error message in response
     buffer but the old goal (with no hyps introduced) in the goals
     buffer. If you processed from the beginning of the buffer you
     wouldn't see anything in the goals buffer. *)

[Matafou]

without this it won't work. This suggests it should be put in some callback instead...

[hendriktews]

I am still trying to understand the problem. When I process the two intro lines together without the patch of this PR, then the goals buffer shows some old goal. Instead, the goals buffer should show the goal before the wrong intro command, that is, the goal after having processed the first intros H.. Is this the problem?

[Matafou]

Yes it is exactly the problem.

there is one way to fix this: to make coqtop -emacs always do "Show" just before printing an error. This was the previous behaviour of coqtop since #188. But it won't work for a few version of emacs.

I experimented an adhoc solution on pg side here.

[chdoc]

Just for the record, there is a possibly related issue of the goals buffer not being updated even after successfully reaching the point, if the point is located right after a comment #204.
(puttering this here for reference following a discussion on Coq-Club today)

[hendriktews]

Pierre, you are extending the action list in the middle of the process filter. Because of the error, the action list has been cleaned already, therefore the show command is sent immediately to Coq, however, Coq needs some time to respond. This is the reason why it won't work without sleeping. Also, as long as you are sitting in the process filter, calling the process filter for the output of the show command is blocked (see proof-shell-filter-wrapper). To deal with this, you parse the output yourself and call a piece of the process filter after waiting (proof-shell-handle-delayed-output). All this looks really fragile IMO.

I would suggest to only insert the show command in the action list and then leave the process filter straight away. When the output arrives, the process filter will be called again and will then take care of it in the usual way. With this approach you'll probably have the problem that the error is not properly signaled any more (the last show was successful after all). To deal with this I would suggest to add appropriate flags and callbacks to the action item and designing new flags and action items if the currently present ones are not sufficient. If you give me some more time, I'll make a proposal.

[Matafou]

Le mer. 11 sept. 2019 à 11:13, hendriktews <[email protected]> a écrit :

Pierre, you are extending the action list in the middle of the process filter. Because of the error, the action list has been cleaned already, therefore the show command is sent immediately to Coq, however, Coq needs some time to respond. This is the reason why it won't work without sleeping. Also, as long as you are sitting in the process filter, calling the process filter for the output of the show command is blocked (see proof-shell-filter-wrapper). To deal with this, you parse the output yourself and call a piece of the process filter after waiting (proof-shell-handle-delayed-output). All this looks really fragile IMO.

Indeed this is.

I would suggest to only insert the show command in the action list and then leave the process filter straight away.When the output arrives, the process filter will be called again and will then take care of it in the usual way.With this approach you'll probably have the problem that the error is not properly signaled any more (the last show was successful after all).

Yes. This would hide the error message.

To deal with this I would suggest to add appropriate flags and callbacks to the action item and designing new flags and action items if the currently present ones are not sufficient. If you give me some more time, I'll make a proposal.

Good idea. Thank you Hendrik. P.

[hendriktews]

and designing new flags and action items if ...

Designing flags and callbacks, of course.

[aa755]

In rare cases (e.g. once in 40 hours of working in company-coq), I used to see this problem EVEN when proof-goto-point did not end in an error or a comment (the 2 known problematic cases). It was very hard to reproduce.
( Usually, the goals involved were huge.)

But now that I run coqtop in a docker container (to use dune cache from a CI job running in an identical docker container), I see this error more than half the times. Here is my "coqtop" which wraps the coqtop in the docker container

[abhishek@optiplex bhv]$ cat /builds/dockerbins/coqtop
#!/bin/bash
docker run --rm -i -v /builds:/builds -w `pwd` -e PATH=/home/coq/.opam/4.14.1+flambda/bin:/usr/lib/llvm/bin/:/home/coq/.local/bin:/home/coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games -e DUNE_CACHE_ROOT=/builds/bedrocksystems/dunecache/dune_cache/dune/db -e LLVM_BASE_DIR=/usr/lib/llvm/bin/ -e CXX=/usr/lib/llvm-14/bin/clang++ -e CC=/usr/lib/llvm-14/bin/clang coq817bhv_uid coqtop "$@"
[abhishek@optiplex bhv]$

I can demonstrate the problem in a zoom call and/or produce instructions to reproduce the issue; the latter would require some administrative approval at my employer but should be doable.

[Matafou]

Great thanks for this work @aa755. I would be happy to take some time to understand the problem. It would be nice if @hendriktews could join because he has some good understanding of the internal loop of PG.

[aa755]

Some update:
I added unbuffer before the call to coqtop and now I cannot trigger the problem anymore. I guess now it is just as rare as it was before, when coqtop used to run in the host and not inside a docker container.

#!/bin/bash
docker run --rm -i -v /builds:/builds -w `pwd` / coq817bhv_uid unbuffer -p coqtop "$@"

It is possible studying what happens without unbuffer and why unbuffer makes a difference could lead do a diagnosis of the rare issue. I will first prepare a public docker image to demonstrate the problem without unbuffer. I should have it ready in a week.

[Matafou]

In itself this gives some clue already. Thanks again for the work.

[aa755]

Sorry, it took longer to produce the reproduction instructions. The following zip file has scripts and .v files to demonstrate the problem:
pgissue.zip
Unzip it to some folder and then run ./setup.sh just one time to set up the docker image. (./setup.sh may emit the error "Error: No such container: fmcontainerbhvbedrock". this is OK.)
Then, run ./demo-stale-proof.sh to see a demo of the "stale proof state" problem. this opens a .v file in emacs. the .v file has further instructions.
In my previous message, I mentioned that after using unbuffer -p, the problem went away. However, unbuffer -p creates another problem: it causes the editor to hang on very large sentences. That problem is illustrated by ./demo-hang.sh

[Matafou]

I finally took some time to have a look. Great job at isolating the bug! Extremely helpful: when looking at the *coq* buffer after processing one line at a time until the first line of the lemma, I see this:

...
<prompt>Coq < 42 || 0 < </prompt>Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).

<prompt>log2_spec < 43 |log2_spec| 0 < </prompt>1 goal (ID 3)
  
  n : N
  ============================
  0 < n -> 2 ^ log2 n <= n < 2 ^ succ (log2 n)

As you can see the prompt comes before the goal! This is very strange and should never happen. It certainly causes the goal not being printed.
Does someone know what could be the cause of this? Is it somehow due to some strange concurrent output buffering in ocaml? It reminds me of what happens when mixing different flavours of Format.printfand Printf.printf for instance. @hendriktews or @erikmd do you have any clue? I guess we will need to ask the coq team if not.

[Matafou]

@ejgallego @gares @maximedenes can you have a look please? Why would coq display the goal after the prompt?

[Matafou]

A bit of context: @aa755 is running coqtop inside a docker image and is getting a strange behaviour where prompt and goals are printed in an unexpected order very frequently.

Things come back to normal if running coqtop with unbuffer -b. However (putting aside that this triggers other issues) this problem also happens (on a much lower frequency) without docker.

So the docker case should help us spot this otherwise rare bug.

Hence the question: why would coq swap goal and prompt printing in any case?

[Matafou]

More info: I can trigger this print swap without the -emacs coqtop option, directly on a terminal.

$ docker run --rm -i -v `pwd`:`pwd` -w `pwd` coqunbuffer coqtop 
Welcome to Coq 8.17.0

Coq < Require Import NArith.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]

Coq < Open Scope N_scope.

Coq < Import N.

Coq < Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).
1 goal
  
  n : N
  ============================
  0 < n -> 2 ^ log2 n <= n < 2 ^ succ (log2 n)

log2_spec < Proof.

log2_spec <  destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.

log2_spec < 6 goals
  
  p : positive
  ============================
  pos (2 ^ Pos.size p) <= pos p~1

goal 2 is:
 pos p~1 < pos (2 ^ Pos.succ (Pos.size p))
goal 3 is:
 pos (2 ^ Pos.size p) <= pos p~0
goal 4 is:
 pos p~0 < pos (2 ^ Pos.succ (Pos.size p))
goal 5 is:
 1 <= 1
goal 6 is:
 1 < pos (2 ^ 1)

[ejgallego]

@Matafou certianly there could be a problem with the flushing, this part has been tricky since 8.5 introduced the feedback mechanism.

First places to look are:

• https://github.com/coq/coq/blob/master/toplevel/coqloop.ml#L332
• https://github.com/coq/coq/blob/master/toplevel/coqloop.ml#L494

I'd try changing the flush order in the first line for example.

[Matafou]

Thanks @ejgallego that makes sense to look there. But my intuition is that printing errors first is correct (error messages are more urgent?). Maybe the problem is that the prompt is printed on error channel... Or is it standard?? It has been like that for decades I suppose...

[ejgallego]

I think printing order is correct, flush order may not be.

[Matafou]

We need this ordering of appearance:

WARNINGS/ERRORS
GOAL
PROMPT

Which suggest IIUC that ERRORS should be flushed first, BUT ALSO that the prompt should not be printed on the error channel, as it is currently.

[ejgallego]

Flushing is per-formatter, also per out channel. Both flushings can race as in it is possible to write to a formatter on out channel o, then later write to the output channel, and flush in reverse inverting the order.

This is a Coq bug so I'd suggest reporting there to see if some Coq developer would like to have a look.

[Matafou]

OK I will submit a bug report.
Of course flushing is per formatter, my question is: why on earth should the prompt be on the error formatter anyways??

[ejgallego]

Of course flushing is per formatter,

Note that this races with the per channel flushing. But it seems the problem here is more about the order of flushing.

That's pretty strange tho, as each of the operations here seem to flush so the order should be preserved.

my question is: why on earth should the prompt be on the error formatter anyways??

I don't know.

[Matafou]

@aa755 can you try https://github.com/Matafou/coq/tree/fix-prompt-err-17753 and see if the bug is fixed?

[aa755]

sure. I will try soon.

[aa755]

In your version (https://github.com/Matafou/coq/tree/fix-prompt-err-17753), after doing ./demo-stale-proof.sh, when I start the coq process by doing C-c enter at some point in the file, my whole emacs just hangs. I am now unable to check even one sentence. Perhaps proof-general also needs to be adapted for the current change?

./demo-hang.sh (which puts unbuffer) works as before: I can start the coq process and check a few sentences but the long definition hangs as before.

You can reproduce it the same way as before, except that I have updated the script to set up the docker image, so that now it installs the custom coq version https://github.com/aa755/pgissuedocker/blob/master/setup.sh