X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Futilities%2Ftest_library.ml;fp=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Futilities%2Ftest_library.ml;h=5cfb7c3487276e2d38f85229e5da13dacd86a7be;hb=ad4b0fa70ccf730e79b0986155f8f58c994570ae;hp=03742ac308a7efc02d68b929158fc5846e169f55;hpb=6e5d56aeaba8db09debf2cb4bfa5afb5b76cdcdc;p=helm.git

diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml
index 03742ac30..5cfb7c348 100644
--- a/helm/software/components/binaries/utilities/test_library.ml
+++ b/helm/software/components/binaries/utilities/test_library.ml
@@ -24,6 +24,7 @@
  *)
 
 let trust = true
+let deadline = 30
 let conffile = "../../../matita/matita.conf.xml"
 
 let _ = CicEnvironment.set_trust (fun _ -> trust);;
@@ -46,6 +47,15 @@ let _ =
      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 =
   try
     Sys.argv.(1)
@@ -74,7 +84,9 @@ let _ =
         flush stdout;
         let uri = UriManager.uri_of_string uri in
         let before = Unix.gettimeofday () in
+        ignore (Unix.alarm deadline);
         ignore (CicTypeChecker.typecheck uri);
+        ignore (Unix.alarm 0);
         let after = Unix.gettimeofday () in
         let diff = after -. before in
         new_total := !new_total +. diff;
@@ -93,16 +105,24 @@ let _ =
               begin
                Printf.printf "SKIPPED\n";
                flush stdout;
-               Printf.eprintf "Continue with next URI? [y/_]";
-               flush stderr;
+               if not !timeout then
+                begin
+                 Printf.eprintf "Continue with next URI? [y/_]";
+                 flush stderr;
+                end;
               end;
-             (match input_line stdin with
-                 "y" -> ()
-               | _ -> raise Done)
+             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 "CIRCULARDEP\n"
         | exn ->
            Printf.printf "FAIL\n";
            flush stdout;