Fix #3934: coqc -time -quick gives unreadable output

Author: maximedenes

lib/system.ml

@@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
   real (round (sstop -. sstart)) ++ str "s" ++
   str ")"
 
-let with_time ~batch f x =
+let with_time ~batch ~header f x =
   let tstart = get_time() in
   let msg = if batch then "" else "Finished transaction in " in
   try
     let y = f x in
     let tend = get_time() in
     let msg2 = if batch then "" else " (successful)" in
-    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if batch then "" else "Finished failing transaction in " in
     let msg2 = if batch then "" else " (failure)" in
-    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 (* We use argv.[0] as we don't want to resolve symlinks *)

lib/system.mli

@@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *)
 
 val fmt_time_difference : time -> time -> Pp.t
 
-val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
+val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b
 
 (** [get_toplevel_path program] builds a complete path to the
    executable denoted by [program]. This involves:

stm/stm.ml

@@ -2017,7 +2017,7 @@ end = struct (* {{{ *)
       find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     Vernacentries.with_fail st fail (fun () ->
-    (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
+    (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
       let Proof.{goals} = Proof.data p in

toplevel/vernac.ml

@@ -37,34 +37,6 @@ let vernac_echo ?loc in_chan = let open Loc in
       Feedback.msg_notice @@ str @@ really_input_string in_chan len
     ) loc
 
-(* For coqtop -time, we display the position in the file,
-   and a glimpse of the executed command *)
-
-let pp_cmd_header {CAst.loc;v=com} =
-  let shorten s =
-    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
-  in
-  let noblank s = String.map (fun c ->
-      match c with
-	| ' ' | '\n' | '\t' | '\r' -> '~'
-	| x -> x
-      ) s
-  in
-  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
-  let safe_pr_vernac x =
-    try Ppvernac.pr_vernac x
-    with e -> str (Printexc.to_string e) in
-  let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
-  in str "Chars " ++ int start ++ str " - " ++ int stop ++
-     str " [" ++ str cmd ++ str "] "
-
-(* This is a special case where we assume we are in console batch mode
-   and take control of the console.
- *)
-let print_cmd_header com =
-  Pp.pp_with !Topfmt.std_ft (pp_cmd_header com);
-  Format.pp_print_flush !Topfmt.std_ft ()
-
 (* Reenable when we get back to feedback printing *)
 (* let is_end_of_input any = match any with *)
 (*     Stm.End_of_input -> true *)
@@ -88,7 +60,6 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
          due to the way it prints. *)
       let com = if state.time
         then begin
-          print_cmd_header com;
           CAst.make ?loc @@ VernacTime(state.time,com)
         end else com in
       let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in

vernac/topfmt.ml

@@ -406,3 +406,24 @@ let with_output_to_file fname func input =
     deep_ft := Util.pi3 old_fmt;
     close_out channel;
     Exninfo.iraise reraise
+
+(* For coqtop -time, we display the position in the file,
+   and a glimpse of the executed command *)
+
+let pr_cmd_header {CAst.loc;v=com} =
+  let shorten s =
+    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+  in
+  let noblank s = String.map (fun c ->
+      match c with
+        | ' ' | '\n' | '\t' | '\r' -> '~'
+        | x -> x
+      ) s
+  in
+  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+  let safe_pr_vernac x =
+    try Ppvernac.pr_vernac x
+    with e -> str (Printexc.to_string e) in
+  let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
+  in str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] "

vernac/topfmt.mli

@@ -71,3 +71,4 @@ val print_err_exn : exn -> unit
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
 
+val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t

vernac/vernacentries.ml

@@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
     control v
   | VernacRedirect (s, {v}) ->
     Topfmt.with_output_to_file s control v
-  | VernacTime (batch, {v}) ->
-    System.with_time ~batch control v;
+  | VernacTime (batch, com) ->
+    let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
+    System.with_time ~batch ~header control com.CAst.v;
 
   and aux ~atts : _ -> unit =
     function