From 789be8e12d78acc622fc9a115c592fa42b8fa3d1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jul 2012 22:58:14 +0000 Subject: [PATCH] Some debugging times exposed. --- matita/components/grafite_engine/grafiteEngine.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 57491cbda..a4942aa07 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -915,8 +915,13 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = let status = List.fold_left (fun status tac -> + let time0 = Unix.gettimeofday () in let status = eval_ng_tac (text,prefix_len,tac) status in - subst_metasenv_and_fix_names status) + let time3 = Unix.gettimeofday () in + HLog.debug ("... eval_ng_tac done in " ^ string_of_float (time3 -. time0) ^ "s"); + let status = subst_metasenv_and_fix_names status in + let time3 = Unix.gettimeofday () in + HLog.debug ("... subst_metasenv_and_fix_names done in " ^ string_of_float (time3 -. time0) ^ "s"); status) status tacl in status -- 2.39.2