From 740e2455d6af62d2eb6fd1bd28acdb429eb5b5f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Jun 2026 16:28:15 +0200 Subject: [PATCH 1/2] Delete unused Topfmt.deep_ft --- vernac/topfmt.ml | 18 +++++------------- vernac/topfmt.mli | 1 - 2 files changed, 5 insertions(+), 14 deletions(-) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b66f8a92c1b5..8791179b14b8 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -72,9 +72,6 @@ let _ = set_dflt_gp !std_ft let err_ft = ref Format.err_formatter let _ = set_gp !err_ft deep_gp -let deep_ft = ref (with_output_to stdout) -let _ = set_gp !deep_ft deep_gp - (* For parametrization through vernacular *) let default = Format.pp_get_max_boxes !std_ft () let default_margin = Format.pp_get_margin !std_ft () @@ -94,14 +91,12 @@ let set_margin v = let v = match v with None -> default_margin | Some v -> v in Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v; Format.pp_set_margin !err_ft v; (* Heuristic, based on usage: the column on the right of max_indent column is 20% of width, capped to 30 characters *) let m = max (64 * v / 100) (v-30) in Format.pp_set_max_indent Format.str_formatter m; Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m; Format.pp_set_max_indent !err_ft m (** Console display of feedback *) @@ -418,25 +413,22 @@ let with_output_to_file ~truncate fname func input = let flags = if truncate then Open_trunc :: flags else flags in open_out_gen flags 0o666 fullfname in - let old_fmt = !std_ft, !err_ft, !deep_ft in + let old_fmt = !std_ft, !err_ft in let new_ft = Format.formatter_of_out_channel channel in set_gp new_ft (get_gp !std_ft); std_ft := new_ft; err_ft := new_ft; - deep_ft := new_ft; try let output = func input in - std_ft := Util.pi1 old_fmt; - err_ft := Util.pi2 old_fmt; - deep_ft := Util.pi3 old_fmt; + std_ft := fst old_fmt; + err_ft := snd old_fmt; Format.pp_print_flush new_ft (); close_out channel; output with reraise -> let reraise = Exninfo.capture reraise in - std_ft := Util.pi1 old_fmt; - err_ft := Util.pi2 old_fmt; - deep_ft := Util.pi3 old_fmt; + std_ft := fst old_fmt; + err_ft := snd old_fmt; Format.pp_print_flush new_ft (); close_out channel; Exninfo.iraise reraise diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 3851a78971eb..e05ba00ffdd5 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -28,7 +28,6 @@ val with_output_to : out_channel -> Format.formatter val std_ft : Format.formatter ref val err_ft : Format.formatter ref -val deep_ft : Format.formatter ref (** {6 For parametrization through vernacular. } *) From 201d836d2f8e74fdd476824e2862dc204dd5a22c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Jun 2026 16:33:01 +0200 Subject: [PATCH 2/2] Update Topfmt.with_output_to_file to use memprof masking API --- vernac/topfmt.ml | 43 +++++++++++++++++++++---------------------- 1 file changed, 21 insertions(+), 22 deletions(-) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 8791179b14b8..136f11859bb5 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -405,33 +405,32 @@ let print_err_exn any = std_logger ?pre_hdr Feedback.Error msg let with_output_to_file ~truncate fname func input = - let fname = String.concat "." [fname; "out"] in - let fullfname = System.get_output_path fname in - System.mkdir (Filename.dirname fullfname); - let channel = - let flags = [Open_wronly; Open_creat; Open_text] in - let flags = if truncate then Open_trunc :: flags else flags in - open_out_gen flags 0o666 fullfname + let acquire () = + let fname = String.concat "." [fname; "out"] in + let fullfname = System.get_output_path fname in + System.mkdir (Filename.dirname fullfname); + let channel = + let flags = [Open_wronly; Open_creat; Open_text] in + let flags = if truncate then Open_trunc :: flags else flags in + open_out_gen flags 0o666 fullfname + in + let old_fmt = !std_ft, !err_ft in + let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); + old_fmt, new_ft, channel in - let old_fmt = !std_ft, !err_ft in - let new_ft = Format.formatter_of_out_channel channel in - set_gp new_ft (get_gp !std_ft); - std_ft := new_ft; - err_ft := new_ft; - try - let output = func input in - std_ft := fst old_fmt; - err_ft := snd old_fmt; - Format.pp_print_flush new_ft (); - close_out channel; - output - with reraise -> - let reraise = Exninfo.capture reraise in + let scope (_, new_ft, channel) = + std_ft := new_ft; + err_ft := new_ft; + func input + in + let release (old_fmt, new_ft, channel) = std_ft := fst old_fmt; err_ft := snd old_fmt; Format.pp_print_flush new_ft (); close_out channel; - Exninfo.iraise reraise + in + Memprof_coq.Masking.with_resource ~acquire () ~scope ~release (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *)