From 684989d19181ff812564ddc5d17f709a7e990cba Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 May 2007 17:29:19 +0000 Subject: [PATCH 1/1] 1. Profiling enabled. 2. Dotfile inserted into log.ma for debugging pourposes. --- .../formal_topology/bin/theory_explorer.ml | 31 ++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml index 0e3e86684..4105893d5 100644 --- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml @@ -1,3 +1,31 @@ +(**** PROFILING ****) +let ok_time = ref 0.0;; +let ko_time = ref 0.0;; + +let profile f x = + let before = Unix.gettimeofday () in + let res = f x in + let after = Unix.gettimeofday () in + let delta = after -. before in + if res = Unix.WEXITED 0 then + ok_time := !ok_time +. delta + else + ko_time := !ko_time +. delta; + res +;; + +let _ = + Sys.catch_break true; + at_exit + (function () -> + prerr_endline + ("\nTIME SPENT IN CHECKING GOOD CONJECTURES: " ^ string_of_float !ok_time); + prerr_endline + ("TIME SPENT IN CHECKING BAD CONJECTURES: " ^ string_of_float !ko_time);) +;; + +(**** END PROFILING ****) + type rel = Equal | SubsetEqual | SupersetEqual let string_of_rel = @@ -174,8 +202,9 @@ let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr = close_out ch; let res = (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*) - Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0 + profile Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0 in + ignore (Unix.system "echo '(*' >> log.ma && cat xxx.dot >> log.ma && echo '*)' >> log.ma"); let ch = open_out_gen [Open_append] 0o0600 "log.ma" in if res then output_string ch (query ^ "\n") -- 2.39.2