helm/software/components/binaries/utilities/test_library.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 let trust = false
  27 let conffile = "../../../matita/matita.conf.xml"
  28
  29 let _ = CicEnvironment.set_trust (fun _ -> trust);;
  30 let _ = Helm_registry.load_from conffile;;
  31
  32 let old_total = ref 0.0
  33 let new_total = ref 0.0
  34
  35 let separator = "============="
  36
  37 let perc newt oldt = (newt -. oldt) /. oldt *. 100.0
  38
  39 let _ =
  40  Sys.catch_break true;
  41  at_exit
  42   (fun () ->
  43     Printf.printf "%s\n" separator;
  44     Printf.printf "Total: %.2f\n" !new_total;
  45     if !old_total <> 0.0 then
  46      Printf.printf "Old: %.2f (%.2f%%)\n" !old_total (perc !new_total !old_total))
  47 ;;
  48
  49 let urifname =
  50   try
  51     Sys.argv.(1)
  52   with Invalid_argument _ ->
  53    prerr_endline "You must supply a file with the list of URIs to check";
  54    exit (-1)
  55
  56 let ic = open_in urifname
  57
  58 let _ =
  59   try
  60     while true do
  61       try
  62         let uri = input_line ic in
  63         if uri = separator then raise End_of_file;
  64         let uri,res,time =
  65          match Str.split (Str.regexp " ") uri with
  66             uri::res::time::_ -> uri, Some res, Some (float_of_string time)
  67           | [ uri ] -> uri, None, None
  68           | _ -> assert false
  69         in
  70         Printf.printf "%s " uri;
  71         let uri = UriManager.uri_of_string uri in
  72         let before = Unix.gettimeofday () in
  73         ignore (CicTypeChecker.typecheck uri);
  74         let after = Unix.gettimeofday () in
  75         let diff = after -. before in
  76         new_total := !new_total +. diff;
  77         Printf.printf "\e[0;32mOK\e[0m %.2f" diff;
  78         (match time with
  79            None -> Printf.printf "\n"
  80          | Some time ->
  81             old_total := !old_total +. time;
  82              Printf.printf " %.2f%%\n" (perc diff time))
  83       with
  84         | End_of_file as exn -> raise exn
  85         | Sys.Break ->
  86            Printf.printf "\e[0;31mSKIPPED\e[0m\n";
  87            flush stdout;
  88            Printf.eprintf "\e[0;31mContinue with next URI? [y/_]\e[0m";
  89            flush stderr;
  90            (match input_line stdin with
  91                "y" -> ()
  92              | _ -> raise Sys.Break)
  93         | exn ->
  94            Printf.printf "\e[0;31mFAIL\e[0m\n";
  95            flush stdout;
  96            prerr_endline (Printexc.to_string exn)
  97     done
  98   with
  99      End_of_file
 100    | Sys.Break -> ()