From d1ca188ac595632aa05281e4d2b523c6c6d3d3a5 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Wed, 14 Oct 2026 18:42:59 +0200
Subject: [PATCH] feat(compile): memory statistics in -tstats

`-tstats <file>` recorded, for each command of the compiled file, its
location and its time. It now also records, as `key=value` fields
after these two, its CPU time, the memory it allocated, the size and
the peak size of the major heap after it, and the number of major
collections during it:

    1:0 7:23 0.083473 cpu=0.080641 alloc=133.550 heap=33.5 top=33.5 gc=1

Sizes are in MB. They come from `Gc.quick_stat`, which costs nothing
noticeable. The peak size of the major heap shows which commands make
a file need its memory, and the allocated memory measures the work of
a command independently of the load of the machine.
---
 src/ec.ml        | 34 ++++++++++++++++++++++++++++------
 src/ecOptions.ml |  2 +-
 2 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/src/ec.ml b/src/ec.ml
index f3bc3467b..7cf2bbc4c 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -714,15 +714,36 @@ let main () =
     | None -> ()
   in
 
-  let tstats : EcLocation.t -> float option -> unit =
+  (* [-tstats]: one line per command, with its location and its time,
+   * then its CPU time, the memory it allocated (in MB), the size and
+   * the peak size of the major heap after it (in MB), and the number of
+   * major collections during it. [tstats ()] starts the measure of a
+   * command, the function it returns records it. *)
+  let tstats : unit -> EcLocation.t -> float option -> unit =
     match options.o_command with
     | `Compile { cmpo_tstats = Some out } ->
         let channel = Format.formatter_of_out_channel (open_out out) in
-        let fmt loc tdelta =
-          Format.fprintf channel "%s %f\n%!"
-            (EcLocation.tostring_raw ~with_fname:false loc) tdelta in
-        fun loc tdelta -> oiter (fmt loc) tdelta
-    | _ -> fun _ _ -> () in
+        let sample () = (Sys.time (), Gc.quick_stat ()) in
+        let mb (words : float) =
+          words *. float_of_int (Sys.word_size / 8) /. (1024. *. 1024.) in
+        let alloc (gc : Gc.stat) =
+          gc.Gc.minor_words +. gc.Gc.major_words -. gc.Gc.promoted_words in
+
+        fun () ->
+          let (cpu0, gc0) = sample () in
+          fun loc tdelta ->
+            let (cpu1, gc1) = sample () in
+            tdelta |> oiter (fun tdelta ->
+              Format.fprintf channel
+                "%s %f cpu=%f alloc=%.3f heap=%.1f top=%.1f gc=%d\n%!"
+                (EcLocation.tostring_raw ~with_fname:false loc) tdelta
+                (cpu1 -. cpu0)
+                (mb (alloc gc1 -. alloc gc0))
+                (mb (float_of_int gc1.Gc.heap_words))
+                (mb (float_of_int gc1.Gc.top_heap_words))
+                (gc1.Gc.major_collections - gc0.Gc.major_collections))
+
+    | _ -> fun () _ _ -> () in
 
   (* Instantiate terminal *)
   let lazy terminal = state.terminal in
@@ -834,6 +855,7 @@ let main () =
                    let timed = p.EP.gl_debug = Some `Timed in
                    let break = p.EP.gl_debug = Some `Break in
                    let ignore_fail = ref false in
+                   let tstats = tstats () in
 
                      state.trace <- state.trace |> Option.map (fun trace ->
                       { State.Trace.trace0 with position = loc.loc_echar } :: trace
diff --git a/src/ecOptions.ml b/src/ecOptions.ml
index a78822aaf..a88d471e9 100644
--- a/src/ecOptions.ml
+++ b/src/ecOptions.ml
@@ -375,7 +375,7 @@ let specs = {
       `Group "loader";
       `Group "provers";
       `Spec  ("gcstats", `Flag  , "Display GC statistics");
-      `Spec  ("tstats" , `String, "Save timing statistics to <file>");
+      `Spec  ("tstats" , `String, "Save timing and memory statistics to <file>");
       `Spec  ("script" , `Flag  , "Computer-friendly output");
       `Spec  ("no-eco" , `Flag  , "Do not cache verification results");
       `Spec  ("trace"  , `Flag  , "Save all goals & messages in .eco");