From 240e678d3acbc5767441f3dc72ee05e20810b33a Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Sun, 12 Jul 2026 10:20:31 +0200
Subject: [PATCH] =?UTF-8?q?perf:=20relax=20OCaml=205.x=20GC=20pacing=20for?=
 =?UTF-8?q?=20custom=20blocks,=20warn=20on=205.0=E2=80=935.3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

EasyCrypt hash-conses its AST and allocates zarith/GMP custom blocks
heavily. On OCaml 5.x the default custom_major_ratio paces the major GC
far too aggressively over that external memory (OCaml issue #14533,
pronounced on 5.5), costing large amounts of CPU for no memory benefit:
compiling a large file (NTTAlgebra.ec) measured ~5x slower than on 4.14
(1255s vs 339s), with the same ~1GB working set.

Set custom_major_ratio to 250 on OCaml >= 5, which restores 4.14-class
performance (5.5: 1255s -> 233s). This is a no-op on 5.4, whose default
pacing is already fine, and harmless there.

Additionally, warn at startup on OCaml 5.0–5.3, whose minor GC
over-promotes values reachable from ephemeron/weak-table keys (OCaml
issue #13643), causing severe memory blowup with EasyCrypt's weak-table
hash-consing. Fixed upstream in OCaml 5.4; recommend upgrading.
---
 src/ec.ml | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/src/ec.ml b/src/ec.ml
index 2b8b6f7d1..f3bc3467b 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -6,6 +6,36 @@ open EcOptions
 module EP = EcParsetree
 module T  = EcTerminal
 
+(* -------------------------------------------------------------------- *)
+(* OCaml runtime version as (major, minor), parsed from [Sys.ocaml_version]. *)
+let ocaml_version : int * int =
+  try Scanf.sscanf Sys.ocaml_version "%d.%d" (fun a b -> (a, b))
+  with _ -> (0, 0)
+
+(* EasyCrypt hash-conses its AST and leans heavily on zarith/GMP custom blocks.
+   On OCaml 5.x the default [custom_major_ratio] paces the major GC far too
+   aggressively over that external memory (OCaml issue #14533, pronounced on
+   5.5), which costs a large amount of CPU for no memory benefit. Relaxing the
+   ratio restores 4.14-class performance. *)
+let tune_gc () =
+  if fst ocaml_version >= 5 then
+    Gc.set { (Gc.get ()) with Gc.custom_major_ratio = 250 }
+
+(* OCaml 5.0-5.3's minor GC over-promotes values reachable from ephemeron /
+   weak-table keys (OCaml issue #13643), causing severe memory blowup with
+   EasyCrypt's weak-table hash-consing. Fixed in OCaml 5.4. *)
+let warn_ocaml_version (terminal : T.terminal) =
+  match ocaml_version with
+  | (5, minor) when minor <= 3 ->
+      T.notice ~immediate:true `Warning
+        (Printf.sprintf
+           "running on OCaml %s: OCaml 5.0-5.3 have a garbage-collector \
+            regression (OCaml issue #13643) that can cause severe memory blowup \
+            in EasyCrypt; please upgrade to OCaml >= 5.4"
+           Sys.ocaml_version)
+        terminal
+  | _ -> ()
+
 (* -------------------------------------------------------------------- *)
 let copyright =
   let sentences =
@@ -117,6 +147,10 @@ let print_config config =
 
 (* -------------------------------------------------------------------- *)
 let main () =
+  (* On OCaml 5.x, relax the major-GC pacing over zarith/GMP custom blocks
+     (see [tune_gc]). *)
+  tune_gc ();
+
   (* When started from Emacs28 on Apple M1, the set of blocks signals *
    * disallows Why3 server to detect external provers completion      *)
   let _ : int list = Unix.sigprocmask Unix.SIG_SETMASK [] in
@@ -708,6 +742,9 @@ let main () =
   if T.interactive terminal then
     T.notice ~immediate:true `Warning copyright terminal;
 
+  (* Warn about GC-regressed OCaml versions (5.0-5.3) *)
+  warn_ocaml_version terminal;
+
   (* Check if a location is past the -upto point *)
   let past_upto (loc : EcLocation.t) =
     match state.upto with