From 890df0f1f7847afafa6a88ab5e3439a5413323ec Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Oct 2022 17:59:23 +0530 Subject: [PATCH] Control.once in debug_profile (#76) --- src/Rewriter/Language/Reify.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v index e2ec4a733..cdad5e998 100644 --- a/src/Rewriter/Language/Reify.v +++ b/src/Rewriter/Language/Reify.v @@ -124,8 +124,8 @@ Module Compilers. := debug_if should_debug_typing_failure_assume_well_typed (fun () => printf "Warning: %s: could not well-type %t due to underlying issue typechecking %t without relevant context %a, but assuming that it's well-typed because %t is not a template-parameter type" funname v term (fun () => Message.of_list Message.of_binder) ctx_tys ty) (). Ltac2 debug_profile (descr : string) (f : unit -> 'a) : 'a := if should_debug_profile () - then Control.time (Some descr) f - else f (). + then Control.once (fun () => Control.time (Some descr) f) + else Control.once f. Ltac2 debug_fine_grained (funname : string) (msg : unit -> message) := debug_if should_debug_fine_grained (fun () => printf "%s: %a" funname (fun () => msg) ()) (). Ltac2 debug_enter_reify (funname : string) (e : constr)