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=1947919aedca4896af2c7893c3b12f926141098c;hb=2a328e2a7623584d5593a9cc547c336c31ad1243;hp=0000000000000000000000000000000000000000;hpb=f5580062e383b1f9737ee30f1ea4459e41106303;p=helm.git

diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml
new file mode 100644
index 000000000..1947919ae
--- /dev/null
+++ b/helm/software/components/binaries/utilities/test_library.ml
@@ -0,0 +1,100 @@
+(* Copyright (C) 2004-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let trust = false
+let conffile = "../../../matita/matita.conf.xml"
+
+let _ = CicEnvironment.set_trust (fun _ -> trust);;
+let _ = Helm_registry.load_from conffile;;
+
+let old_total = ref 0.0
+let new_total = ref 0.0
+
+let separator = "=============" 
+
+let perc newt oldt = (newt -. oldt) /. oldt *. 100.0
+
+let _ =
+ Sys.catch_break true;
+ at_exit
+  (fun () ->
+    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))
+;;
+
+let urifname =
+  try
+    Sys.argv.(1)
+  with Invalid_argument _ ->
+   prerr_endline "You must supply a file with the list of URIs to check";
+   exit (-1)
+
+let ic = open_in urifname
+
+let _ =
+  try
+    while true do
+      try
+        let uri = input_line ic in
+        if uri = separator then raise End_of_file;
+        let uri,res,time =
+         match Str.split (Str.regexp " ") uri with
+            uri::res::time::_ -> uri, Some res, Some (float_of_string time)
+          | [ uri ] -> uri, None, None
+          | _ -> assert false
+        in
+        Printf.printf "%s " uri;
+        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
+        new_total := !new_total +. diff;
+        Printf.printf "OK %.2f" diff;
+        (match time with
+           None -> Printf.printf "\n"
+         | Some time ->
+            old_total := !old_total +. time;
+             Printf.printf " %.2f%%\n" (perc diff time))
+      with
+        | End_of_file as exn -> raise exn
+        | Sys.Break ->
+           Printf.printf "SKIPPED\n";
+           flush stdout;
+           Printf.eprintf "Continue with next URI? [y/_]";
+           flush stderr;
+           (match input_line stdin with
+               "y" -> ()
+             | _ -> raise Sys.Break)
+        | exn ->
+           Printf.printf "FAIL\n";
+           flush stdout;
+           prerr_endline (Printexc.to_string exn)
+    done
+  with
+     End_of_file
+   | Sys.Break -> ()