Pierre Courtieu
Pierre Courtieu
Duplicate of #357.
Hi Hendrik. Seems to work like charm here (ocaml 4.14.1, coq 8.15.1). One remark on compiling prooftree: configure.sh displays an error: ``` test ocamlopt.opt -I +lablgtk2 File "_none_", line 1:...
> > One remark on compiling prooftree: configure.sh displays an error: > I agree it is confusing, but it also printed `Configuration successful` at the end, didn't it? Yes. >...
@hendriktews do we merge this?
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...
In itself this gives some clue already. Thanks again for the work.
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...
@ejgallego @gares @maximedenes can you have a look please? Why would coq display the goal *after* the prompt?
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....
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...