[stm] Tweak debug options.

We allow for a dynamic setting of the STM debug flag, and we print
some more information about the result of `process_transaction`.

We also fix a printing bug due to mixing `Printf` and `Format`, which
are not compatible.

6 files changed, 21 insertions, 8 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 00f515b5a..b2671e5b6 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -80,6 +80,8 @@ let async_proofs_is_master () =
 let async_proofs_delegation_threshold = ref 0.03
 
 let debug = ref false
+let stm_debug = ref false
+
 let in_debugger = ref false
 let in_toplevel = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 0b00ac13c..7ce808041 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -49,6 +49,9 @@ val debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
 
+(** Enable STM debugging *)
+val stm_debug : bool ref
+
 val profile : bool
 
 (* Legacy flags *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 84c8aa9a9..bf5647771 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -7,13 +7,14 @@
 (************************************************************************)
 
 (* enable in case of stm problems  *)
-let stm_debug = false
+(* let stm_debug () = !Flags.debug *)
+let stm_debug () = !Flags.stm_debug
 
-let stm_pr_err s  = Printf.eprintf "%s] %s\n"     (System.process_id ()) s; flush stderr
-let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
+let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (System.process_id ()) s
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp
 
-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_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 ()
 
@@ -330,7 +331,7 @@ end = struct (* {{{ *)
 
        In case you are hitting the race enable stm_debug.
     *)
-    if stm_debug then Flags.we_are_parsing := false;
+    if stm_debug () then Flags.we_are_parsing := false;
 
     let fname =
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
@@ -2641,7 +2642,11 @@ let process_transaction ?(newtip=Stateid.fresh ())
       | VtUnknown, VtLater ->
           anomaly(str"classifier: VtUnknown must imply VtNow")
     end in
-    stm_prerr_endline (fun () -> "processed }}}");
+    let pr_rc rc = match rc with
+      | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
+      | _   -> Pp.(str "unfocus")
+    in
+    stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}");
     VCS.print ();
     rc
   with e ->
@@ -2681,7 +2686,7 @@ let parse_sentence sid pa =
       (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
        str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
        str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
-  if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug then
+  if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then
     Feedback.msg_debug
       (str "Warning, the real tip doesn't match the current tip." ++
        str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 552a943c8..b0a5ce7a1 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -96,6 +96,7 @@ let parse_args () =
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
+      |"-stm-debug"
       as o) :: rem ->
 	parse (cfiles,o::args) rem
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f50bfb3d..f1588b768 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -555,6 +555,7 @@ let parse_args arglist =
     |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
     |"-debug" -> set_debug ()
+    |"-stm-debug" -> Flags.stm_debug := true
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e29048035..feaf207b1 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -69,6 +69,7 @@ let print_usage_channel co command =
 \n  -boot                  boot mode (implies -q and -batch)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
+\n  -stm-debug             STM debug mode (will trace every transaction) \
 \n  -emacs                 tells Coq it is executed under Emacs\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\