when OCAML_GC_STATS points to a filepath, write Gc stats into it

This interface is promoted by the operf-macro tool
  https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.

Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
  but in a Coq-implementation-defined format that is not suitable
  for across-programs comparison
  (also an environment variable allows to profile Coq runs on any .v,
   in an non-intrusive way)

Note to the Github Robot:
This closes #75

1 files changed, 14 insertions, 2 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b706a81e6..d88ba23ea 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -100,9 +100,21 @@ let output_context = ref false
 let memory_stat = ref false
 
 let print_memory_stat () =
-  if !memory_stat then
+  begin (* -m|--memory from the command-line *)
+    if !memory_stat then
     ppnl
-      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+  end;
+  begin
+    (* operf-macro interface:
+       https://github.com/OCamlPro/operf-macro *)
+    try
+      let fn = Sys.getenv "OCAML_GC_STATS" in
+      let oc = open_out fn in
+      Gc.print_stat oc;
+      close_out oc
+    with _ -> ()
+  end
 
 let _ = at_exit print_memory_stat