]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
bumped changelog line to match upload date
[helm.git] / helm / gTopLevel / testlibrary.ml
index ea6e4c6c037db42b62fb335e94a6776bc9d7546a..fccdc19c619530b67093437c77a00254b2534869 100644 (file)
@@ -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 ()
 
@@ -12,7 +15,7 @@ let verbose = false
 exception Failure of string
 let fail msg = raise (Failure msg)
 
-let uri_predicate = ref BatchParser.constants_only
+let uri_predicate = ref (BatchParser.constants_only ~prefix:"")
 
 module DisambiguateCallbacks =
  struct
@@ -88,16 +91,35 @@ 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
+      `Nok*)
+  | exn -> raise exn
 
-let report (ok,nok,maybe) =
+let report (ok,nok,maybe,timeout) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
@@ -106,9 +128,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 +146,9 @@ let do_uri (ok, nok, maybe) uri =
   | `Maybe ->
       print_endline "\e[01;33m[  MANY  ]\e[00m";
       maybe := uri_str :: !maybe
+  | `TimeOut ->
+      print_endline "\e[01;34m[TIMEOUT!]\e[00m";
+      timeout := uri_str :: !timeout
 
 let do_file status fname =
   try
@@ -147,19 +175,26 @@ let _ =
        (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
-  let varsprefix = ref "" in
+  let prefix = ref "" in
+  let varsprefix = ref "####" in
   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
   let spec =
     [ "-vars", Arg.Set tryvars, "try also variables" ;
       "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
+      "-prefix", Arg.Set_string prefix,
+        "limit object choices to URIs beginning with prefix" ; 
       "-varsprefix", Arg.Set_string varsprefix,
-        "limit variable choices to URIs beginning with prefix" ;
+        "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;
   let names = List.rev !names in
-  uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix;
-  let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
+  if !varsprefix = "####" then varsprefix := !prefix ;
+  uri_predicate :=
+   BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
+  let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
   List.iter
     (fun name ->
       try