Skip to content

Commit

Permalink
Fix coq#17753 coqtop output is sometimes incorrecty ordered.
Browse files Browse the repository at this point in the history
Which seems to cause [this PG
bug](ProofGeneral/PG#429 (comment)).
  • Loading branch information
Matafou committed Jun 20, 2023
1 parent 8768ba3 commit 45cc5ed
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions toplevel/coqloop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ let print_emacs = ref false

let top_stderr x =
Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
let top_std x =
Format.fprintf !Topfmt.std_ft "@[%a@]%!" pp_with x

(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)
Expand Down Expand Up @@ -59,7 +61,7 @@ let prompt_char doc ic ibuf count =
| ll::_ -> Int.equal ibuf.len ll
| [] -> Int.equal ibuf.len 0
in
if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc));
if bol && not !print_emacs then top_std (str (ibuf.prompt doc));
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
Expand Down Expand Up @@ -331,9 +333,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
(* This mimics the semantics of the old Pp.flush_all *)
let loop_flush_all () =
flush stderr;
Format.pp_print_flush !Topfmt.err_ft ();
flush stdout;
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
Format.pp_print_flush !Topfmt.std_ft ()

(* Goal equality heuristic. *)
let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
Expand Down Expand Up @@ -493,7 +495,7 @@ let rec vernac_loop ~state =
let open Vernac.State in
loop_flush_all ();
top_stderr (fnl());
if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
if !print_emacs then top_std (str (top_buffer.prompt state.doc));
resynch_buffer top_buffer;
let state, drop = read_and_execute ~state in
if drop then state else (vernac_loop [@ocaml.tailcall]) ~state
Expand Down

1 comment on commit 45cc5ed

@Matafou
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Forget this, it was based on coq branch v8.17 instead of master.

Please sign in to comment.