Serious test for the Coq library added (name test_library).

Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.

diff --git a/components/binaries/utilities/Makefile b/components/binaries/utilities/Makefile
index c22d2a99d962562a07e55f4ed58421dad812920d..314136db57dabda1d015fd7df4f030898d4c8e53 100644 (file)
--- a/components/binaries/utilities/Makefile
+++ b/components/binaries/utilities/Makefile
@@ -1,6 +1,6 @@
 H=@
 
-UTILITIES = create_environment parse_library list_uris
+UTILITIES = create_environment parse_library list_uris test_library
 UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES))
 LINKOPTS = -linkpkg -thread
 LIBS = helm-cic_proof_checking

diff --git a/components/binaries/utilities/test_library.ml b/components/binaries/utilities/test_library.ml
new file mode 100644 (file)
index 0000000..1947919
--- /dev/null
+++ b/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 "\e[0;32mOK\e[0m %.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 "\e[0;31mSKIPPED\e[0m\n";
+           flush stdout;
+           Printf.eprintf "\e[0;31mContinue with next URI? [y/_]\e[0m";
+           flush stderr;
+           (match input_line stdin with
+               "y" -> ()
+             | _ -> raise Sys.Break)
+        | exn ->
+           Printf.printf "\e[0;31mFAIL\e[0m\n";
+           flush stdout;
+           prerr_endline (Printexc.to_string exn)
+    done
+  with
+     End_of_file
+   | Sys.Break -> ()