X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=ee1b982c41547aa6526628997d646226e316f52f;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=af459000a0c18e44de8f41e20b1f14e16e4dc5e6;hpb=6cfcba76baa8f30c42624e911bd34a702f785766;p=helm.git

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index af459000a..ee1b982c4 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,9 +1,12 @@
 
 open Printf
 
+let time_out = ref 5;;
+
 Helm_registry.load_from "gTopLevel.conf.xml";;
 
-let mqi_debug_fun = ignore
+let mqi_debug_fun s =
+ HelmLogger.log ~append_NL:true (`Msg (`T s))
 let mqi_flags = []
 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
 
@@ -88,16 +91,33 @@ let test_uri uri =
       debug_print "AInductiveDefinition: boh ..." ;
       assert false
 
+exception TimeOut;;
+                                                                                
+ignore
+ (Sys.signal Sys.sigalrm
+   (Sys.Signal_handle
+     (fun _ ->
+       (* We do this in case that some "with _" intercepts the first exception *)
+       ignore (Unix.alarm 1) ;
+       raise TimeOut)))
+;;
+
+
 let test_uri uri =
   try
+   ignore (Unix.alarm !time_out) ;
    if test_uri uri = 1 then `Ok else `Maybe
   with
+  | TimeOut ->
+     (* We do this to clear the alarm set by the signal handler *)
+     ignore (Unix.alarm 0) ;
+     `TimeOut
   | exn ->
       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
         (Printexc.to_string exn));
       `Nok
 
-let report (ok,nok,maybe) =
+let report (ok,nok,maybe,timeout) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
@@ -106,9 +126,12 @@ let report (ok,nok,maybe) =
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
   print_endline "Multiple answers URIs:";
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
+  print_newline ();
+  print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
   print_newline ()
 
-let do_uri (ok, nok, maybe) uri =
+let do_uri (ok, nok, maybe, timeout) uri =
   let uri_str = UriManager.string_of_uri uri in
   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
   match test_uri uri with
@@ -121,6 +144,9 @@ let do_uri (ok, nok, maybe) uri =
   | `Maybe ->
       print_endline "[  MANY  ]";
       maybe := uri_str :: !maybe
+  | `TimeOut ->
+      print_endline "[TIMEOUT!]";
+      timeout := uri_str :: !timeout
 
 let do_file status fname =
   try
@@ -157,6 +183,8 @@ let _ =
         "limit object choices to URIs beginning with prefix" ; 
       "-varsprefix", Arg.Set_string varsprefix,
         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
+      "-timeout", Arg.Set_int time_out,
+       "number of seconds before a timeout; 0 means no timeout"
     ]
   in
   Arg.parse spec (fun name -> names := name :: !names) usage;
@@ -164,7 +192,7 @@ let _ =
   if !varsprefix = "####" then varsprefix := !prefix ;
   uri_predicate :=
    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
-  let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
+  let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
   List.iter
     (fun name ->
       try