From: Claudio Sacerdoti Coen Date: Thu, 30 Mar 2006 11:40:40 +0000 (+0000) Subject: Added deadline (now 30s) to each test. X-Git-Tag: make_still_working~7443 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad4b0fa70ccf730e79b0986155f8f58c994570ae;p=helm.git Added deadline (now 30s) to each test. --- 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;