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 exception Done;;
  59
  60 let _ =
  61   try
  62     while true do
  63       try
  64         let uri = input_line ic in
  65         if uri = separator then raise End_of_file;
  66         let uri,res,time =
  67          match Str.split (Str.regexp " ") uri with
  68             uri::res::time::_ -> uri, Some res, Some (float_of_string time)
  69           | [uri;res] -> uri, Some res, None
  70           | [ uri ] -> uri, None, None
  71           | _ -> assert false
  72         in
  73         Printf.printf "%s " uri;
  74         flush stdout;
  75         let uri = UriManager.uri_of_string uri in
  76         let before = Unix.gettimeofday () in
  77         ignore (CicTypeChecker.typecheck uri);
  78         let after = Unix.gettimeofday () in
  79         let diff = after -. before in
  80         new_total := !new_total +. diff;
  81         Printf.printf "\e[0;32mOK\e[0m %.2f" diff;
  82         (match time with
  83            None -> Printf.printf "\n"
  84          | Some time ->
  85             old_total := !old_total +. time;
  86              Printf.printf " %.2f%%\n" (perc diff time))
  87       with
  88         | End_of_file as exn -> raise exn
  89         | Sys.Break ->
  90            let rec skip_break prompt =
  91             try
  92              if prompt then
  93               begin
  94                Printf.printf "\e[0;31mSKIPPED\e[0m\n";
  95                flush stdout;
  96                Printf.eprintf "\e[0;31mContinue with next URI? [y/_]\e[0m";
  97                flush stderr;
  98               end;
  99              (match input_line stdin with
 100                  "y" -> ()
 101                | _ -> raise Done)
 102             with
 103              Sys.Break -> skip_break false
 104            in
 105             skip_break true
 106         | exn ->
 107            Printf.printf "\e[0;31mFAIL\e[0m\n";
 108            flush stdout;
 109            prerr_endline (Printexc.to_string exn)
 110     done
 111   with
 112      End_of_file
 113    | Done -> ()