Added a Print Debug GC command that displays the current state of

the OCaml GC, as indicated by [Gc.stat].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 27 insertions, 0 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bbb68689c3..d19857ee1c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -45,6 +45,7 @@ type printable =
   | PrintNamespace of DirPath.t
   | PrintMLLoadPath
   | PrintMLModules
+  | PrintDebugGC
   | PrintName of reference or_by_notation
   | PrintGraph
   | PrintClasses
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index aac47126fc..f4380c9d7d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -829,6 +829,7 @@ GEXTEND Gram
 
       | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath
       | IDENT "ML"; IDENT "Modules" -> PrintMLModules
+      | IDENT "Debug"; IDENT "GC" -> PrintDebugGC
       | IDENT "Graph" -> PrintGraph
       | IDENT "Classes" ->  PrintClasses
       | IDENT "TypeClasses" -> PrintTypeClasses
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3e6fa48615..2ba972b5dc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -430,6 +430,7 @@ let pr_printable = function
 | PrintModules -> str "Print Modules"
 | PrintMLLoadPath -> str "Print ML Path"
 | PrintMLModules -> str "Print ML Modules"
+| PrintDebugGC -> str "Print ML GC"
 | PrintGraph -> str "Print Graph"
 | PrintClasses -> str "Print Classes"
 | PrintTypeClasses -> str "Print TypeClasses"
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 1909f6809c..1e0bbbcf3d 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -358,3 +358,25 @@ let print_ml_path () =
 let print_ml_modules () =
   let l = get_loaded_modules () in
   str"Loaded ML Modules: " ++ pr_vertical_list str l
+
+let print_gc () =
+  let stat = Gc.stat () in
+  let msg =
+    str "minor words: " ++ real stat.Gc.minor_words ++ fnl () ++
+    str "promoted words: " ++ real stat.Gc.promoted_words ++ fnl () ++
+    str "major words :" ++ real stat.Gc.major_words ++ fnl () ++
+    str "minor_collections: " ++ int stat.Gc.minor_collections ++ fnl () ++
+    str "major_collections: " ++ int stat.Gc.major_collections ++ fnl () ++
+    str "heap_words: " ++ int stat.Gc.heap_words ++ fnl () ++
+    str "heap_chunks: " ++ int stat.Gc.heap_chunks ++ fnl () ++
+    str "live_words: " ++ int stat.Gc.live_words ++ fnl () ++
+    str "live_blocks: " ++ int stat.Gc.live_blocks ++ fnl () ++
+    str "free_words: " ++ int stat.Gc.free_words ++ fnl () ++
+    str "free_blocks: " ++ int stat.Gc.free_blocks ++ fnl () ++
+    str "largest_free: " ++ int stat.Gc.largest_free ++ fnl () ++
+    str "fragments: " ++ int stat.Gc.fragments ++ fnl () ++
+    str "compactions: " ++ int stat.Gc.compactions ++ fnl () ++
+    str "top_heap_words: " ++ int stat.Gc.top_heap_words ++ fnl () ++
+    str "stack_size: " ++ int stat.Gc.stack_size
+  in
+  hv 0 msg
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 3696a654f2..1b9257c617 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -65,3 +65,4 @@ val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
 val print_ml_path : unit -> Pp.std_ppcmds
 val print_ml_modules : unit -> Pp.std_ppcmds
+val print_gc : unit -> Pp.std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 103253c527..3981d17a92 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1429,6 +1429,7 @@ let vernac_print = function
   | PrintNamespace ns -> print_namespace ns
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
+  | PrintDebugGC -> msg_notice (Mltop.print_gc ())
   | PrintName qid -> dump_global qid; msg_notice (print_name qid)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())