matitaprover is now flexible enough to allow the computation of statistics on

[helm.git] / helm / software / components / binaries / utilities / test_library.ml

diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml
index 1947919aedca4896af2c7893c3b12f926141098c..98ade3adb54ad8a8e408d8771808efbb02a37d08 100644 (file)
--- a/helm/software/components/binaries/utilities/test_library.ml
+++ b/helm/software/components/binaries/utilities/test_library.ml
@@ -23,7 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
-let trust = false
+let trust = true
+let deadline = 30
 let conffile = "../../../matita/matita.conf.xml"
 
 let _ = CicEnvironment.set_trust (fun _ -> trust);;
@@ -43,7 +44,16 @@ let _ =
     Printf.printf "%s\n" separator;
     Printf.printf "Total: %.2f\n" !new_total;
     if !old_total <> 0.0 then
-     Printf.printf "Old: %.2f (%.2f)\n" !old_total (perc !new_total !old_total))
+     Printf.printf "Old: %.2f (%.2f%%)\n" !old_total (perc !new_total !old_total))
+;;
+
+let timeout = ref false;;
+
+let _ =
+ Sys.set_signal 14 (* SIGALRM *)
+  (Sys.Signal_handle (fun _ ->
+    timeout := true;
+    raise Sys.Break))
 ;;
 
 let urifname =
@@ -55,6 +65,8 @@ let urifname =
 
 let ic = open_in urifname
 
+exception Done;;
+
 let _ =
   try
     while true do
@@ -64,15 +76,33 @@ let _ =
         let uri,res,time =
          match Str.split (Str.regexp " ") uri with
             uri::res::time::_ -> uri, Some res, Some (float_of_string time)
+          | [uri;res] -> uri, Some res, None
           | [ uri ] -> uri, None, None
           | _ -> assert false
         in
         Printf.printf "%s " uri;
+        flush stdout;
         let uri = UriManager.uri_of_string uri in
-        let before = Unix.gettimeofday () in
-        ignore (CicTypeChecker.typecheck uri);
-        let after = Unix.gettimeofday () in
-        let diff = after -. before in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        ignore (Unix.alarm deadline);
+        CicTypeChecker.typecheck_obj uri obj;
+        ignore (Unix.alarm 0);
+        CicEnvironment.remove_obj uri;
+        let before = Unix.times () in
+        ignore (Unix.alarm deadline);
+        ignore (CicTypeChecker.typecheck_obj uri obj);
+        ignore (Unix.alarm 0);
+        let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in
+        if memusage > 500 then
+         begin
+          prerr_endline ("MEMORIA ALLOCATA: " ^ string_of_int memusage ^ "Mb");
+          CicEnvironment.empty ();
+          Gc.compact ();
+          let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in
+            prerr_endline ("DOPO CicEnvironment.empty: " ^ string_of_int memusage ^ "Mb");
+         end;
+        let after = Unix.times () in
+        let diff = after.Unix.tms_utime +. after.Unix.tms_stime -. before.Unix.tms_utime -. before.Unix.tms_stime in
         new_total := !new_total +. diff;
         Printf.printf "\e[0;32mOK\e[0m %.2f" diff;
         (match time with
@@ -83,18 +113,41 @@ let _ =
       with
         | End_of_file as exn -> raise exn
         | Sys.Break ->
-           Printf.printf "\e[0;31mSKIPPED\e[0m\n";
-           flush stdout;
-           Printf.eprintf "\e[0;31mContinue with next URI? [y/_]\e[0m";
-           flush stderr;
-           (match input_line stdin with
-               "y" -> ()
-             | _ -> raise Sys.Break)
+           let rec skip_break prompt =
+            try
+             if prompt then
+              begin
+               Printf.printf "\e[0;31mSKIPPED\e[0m\n";
+               flush stdout;
+               if not !timeout then
+                begin
+                 Printf.eprintf "\e[0;31mContinue with next URI? [y/_]\e[0m";
+                 flush stderr;
+                end;
+              end;
+             if not !timeout then
+              (match input_line stdin with
+                  "y" -> ()
+                | _ -> raise Done)
+             else
+              timeout := false
+            with
+             Sys.Break -> skip_break false
+           in
+            skip_break true
+        | CicEnvironment.CircularDependency _ ->
+           Printf.printf "\e[0;31mCIRCULARDEP\e[0m\n"
         | exn ->
            Printf.printf "\e[0;31mFAIL\e[0m\n";
            flush stdout;
-           prerr_endline (Printexc.to_string exn)
+           prerr_endline
+            (match exn with
+                CicTypeChecker.TypeCheckerFailure msg ->
+                 "TypeCheckerFailure: " ^ Lazy.force msg
+              | CicTypeChecker.AssertFailure msg ->
+                 "TypeCheckerAssertion: " ^ Lazy.force msg
+              | _ -> Printexc.to_string exn)
     done
   with
      End_of_file
-   | Sys.Break -> ()
+   | Done -> ()