diff options
| author | Maxime Dénès | 2020-10-15 15:31:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-24 15:09:15 +0100 |
| commit | 068031ff7da092c1e2d35db27d713b9606960c42 (patch) | |
| tree | 2a3e2ae6a82e60a76ef31659ff305d70a4b2ea39 /stm | |
| parent | 264aba2484312a2172cd36dd9b89ed66e4f38864 (diff) | |
Infrastructure for fine-grained debug flags
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/spawned.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 8 |
3 files changed, 6 insertions, 6 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4c4c26f47e..dd80ff21aa 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -13,7 +13,7 @@ open Pp open Util let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () +let stm_prerr_endline s = if CDebug.(get_flag misc) then begin stm_pr_err (str s) end else () type cancel_switch = bool ref let async_proofs_flags_for_workers = ref [] diff --git a/stm/spawned.ml b/stm/spawned.ml index 5cc8be78f5..ee9c8e9942 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -11,7 +11,7 @@ open Spawn let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type chandescr = AnonPipe | Socket of string * int * int diff --git a/stm/stm.ml b/stm/stm.ml index 7de109e596..5ed6adbd63 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -9,7 +9,7 @@ (************************************************************************) (* enable in case of stm problems *) -(* let stm_debug () = !Flags.debug *) +(* let stm_debug () = CDebug.(get_flag misc) *) let stm_debug = ref false let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s @@ -18,7 +18,7 @@ let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.p let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () -let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if CDebug.(get_flag misc) then begin stm_pr_err (s ()) end else () open Pp open CErrors @@ -785,7 +785,7 @@ end = struct (* {{{ *) end let print ?(now=false) () = - if !Flags.debug then NB.command ~now (print_dag !vcs) + if CDebug.(get_flag misc) then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -1533,7 +1533,7 @@ end = struct (* {{{ *) when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *) Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n)) | Some _, Some s -> - if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state"); + if CDebug.(get_flag misc) then msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function |