Merge pull request #955 from coq/log-force

toplevel: always print fatal exception
coq · Dec 5, 2024 · 3221018 · 3221018
2 parents 49dda14 + dfbfc71
commit 3221018
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 10 deletions.
diff --git a/language-server/dm/delegationManager.ml b/language-server/dm/delegationManager.ml
@@ -105,7 +105,7 @@ module type Worker = sig
   val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 
   (* CDebug aware print *)
-  val log : string -> unit
+  val log : ?force:bool -> string -> unit
 
 end
 

diff --git a/language-server/dm/delegationManager.mli b/language-server/dm/delegationManager.mli
@@ -88,7 +88,7 @@ module type Worker = sig
    val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 
    (* CDebug aware print *)
-   val log : string -> unit
+   val log : ?force:bool -> string -> unit
 
 end
 

diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
@@ -94,5 +94,5 @@ module ProofWorkerProcess : sig
    val parse_options : Coqargs.t -> string list -> options * string list
 [%%endif]
   val main : st:Vernacstate.t -> options -> unit
-  val log : string -> unit
+  val log : ?force:bool -> string -> unit
 end
diff --git a/language-server/dm/log.ml b/language-server/dm/log.ml
@@ -49,8 +49,8 @@ let mk_log name =
   let flag = is_enabled name (Array.to_list Sys.argv) in
   let flag_init = is_enabled "init" (Array.to_list Sys.argv) in
   write_to_init_log ("log " ^ name ^ " is " ^ if flag then "on" else "off");
-  Log (fun msg ->
-    let should_print_log = flag || (flag_init && not !lsp_initialization_done) in
+  Log (fun ?(force=false) msg ->
+    let should_print_log = force || flag || (flag_init && not !lsp_initialization_done) in
     if should_print_log then begin
       let txt = Format.asprintf "[%-20s, %d, %f] %s" name (Unix.getpid ()) (Unix.gettimeofday ()) msg in
       if not !lsp_initialization_done then begin

diff --git a/language-server/dm/log.mli b/language-server/dm/log.mli
@@ -14,7 +14,7 @@
 
 open Types
 
-val mk_log : string -> (string -> unit) log
+val mk_log : string -> (?force:bool -> string -> unit) log
 val logs : unit -> string list
 
 type event = string

diff --git a/language-server/dm/parTactic.mli b/language-server/dm/parTactic.mli
@@ -19,7 +19,7 @@ module TacticWorkerProcess : sig
    val parse_options : Coqargs.t -> string list -> options * string list
 [%%endif]
   val main : st:Vernacstate.t -> options -> unit
-  val log : string -> unit
+  val log : ?force:bool -> string -> unit
 end
 
 (* HACK: the sentence id of the current phrase is used to report errors *)

diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
@@ -33,9 +33,9 @@ let loop () =
   try loop todo
   with exn ->
     let info = Exninfo.capture exn in
-    log "==========================================================";
-    log @@ Pp.string_of_ppcmds @@ CErrors.iprint_no_report info;
-    log "=========================================================="
+    log ~force:true "==========================================================";
+    log ~force:true @@ Pp.string_of_ppcmds @@ CErrors.iprint_no_report info;
+    log ~force:true "=========================================================="
 
 let vscoqtop_specific_usage = {
   Boot.Usage.executable_name = "vscoqtop";