snapshot for release

diff --git a/matita/library/list/list.ma b/matita/library/list/list.ma
index ffa2c8ef9ac106c007f701cef1cf21b589f51a19..bb341d245fad82a43657e4e427956968fac8b3c2 100644 (file)
--- a/matita/library/list/list.ma
+++ b/matita/library/list/list.ma
@@ -92,6 +92,29 @@ theorem cons_append_commute:
   reflexivity;
 qed.
 
+inductive permutation (A:Set) : list A -> list A -> Prop \def
+  | refl : \forall l:list A. permutation ? l l
+  | swap : \forall l:list A. \forall x,y:A. 
+              permutation ? (x :: y :: l) (y :: x :: l)
+  | trans : \forall l1,l2,l3:list A.
+              permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
+with permut1 : list A -> list A -> Prop \def
+  | step : \forall l1,l2:list A. \forall x,y:A. 
+      permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).
+
+include "nat/nat.ma".  
+   
+definition x1 \def S O.
+definition x2 \def S x1.
+definition x3 \def S x2.
+   
+theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
+  apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
+  apply refl.
+  apply (step ? (x1::[]) [] x2 x3).
+  qed. 
+
+
 (*
 theorem nil_append_nil_both:
   \forall A:Set.\forall l1,l2:list A.

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index 06f7815b912e3669e6004855445e4fa47cbd8f2d..f66ec6aff40544c39285849053b7047dfd05363c 100644 (file)
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -52,6 +52,7 @@ let registry_defaults = [
   "matita.profile",           "true";
   "matita.system",            "false";
   "matita.verbosity",         "1";
+  "matita.bench",              "false";
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]
@@ -237,6 +238,9 @@ let parse_cmdline init_status =
         "-noprofile", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
           "Turns off profiling printings";
+        "-bench", 
+          Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
+          "Turns on timing prints";
         "-preserve",
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
           "Turns off automatic baseuri cleaning";

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 8135e24727ac6d79579e48be9f8dc9e00ab2c272..ca587690cfecf60a2bd332b6164d37f416f9b93d 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -153,11 +153,46 @@ let go () =
   Sys.catch_break true;
   interactive_loop ()
 
+let pp_times fname bench_mode rc big_bang = 
+  if bench_mode then
+    begin
+      let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
+      let r = Unix.gettimeofday () -. big_bang in
+      let extra = try Sys.getenv "DO_TESTS_EXTRA" with Not_found -> "" in
+      let cc = 
+        if Str.string_match (Str.regexp "opt$") Sys.argv.(0) 0 then 
+          "matitac.opt" 
+        else 
+          "matitac" 
+      in
+      let rc = if rc then "OK" else "FAIL" in
+      let times = 
+        let fmt t = 
+          let seconds = int_of_float t in
+          let cents = int_of_float ((t -. floor t) *. 100.0) in
+          let minutes = seconds / 60 in
+          let seconds = seconds mod 60 in
+          Printf.sprintf "%2dm%02d.%02ds" minutes seconds cents
+        in
+        Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
+      in
+      let s = 
+        Printf.sprintf "%s\t%-30s   %s\t%s\t%s" cc fname rc times extra 
+      in
+      print_endline s;
+      flush stdout
+    end
+;;
+
 let main ~mode = 
+  let big_bang = Unix.gettimeofday () in
   MatitaInit.initialize_all ();
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
   let system_mode =  Helm_registry.get_bool "matita.system" in
+  let bench_mode =  Helm_registry.get_bool "matita.bench" in
+  if bench_mode then
+    Helm_registry.set_int "matita.verbosity" 0;
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
   grafite_status := Some (GrafiteSync.init ());
@@ -174,10 +209,16 @@ let main ~mode =
   in
   if Helm_registry.get_int "matita.verbosity" < 1 then
     HLog.set_log_callback newcb;
+  if bench_mode then
+    begin
+    HLog.set_log_callback (fun _ _ -> ());
+    let out = open_out "/dev/null" in
+    Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
+    end;
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
     let time = Unix.time () in
-    if Helm_registry.get_int "matita.verbosity" < 1 then
+    if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then
       origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
     else
       HLog.message (sprintf "execution of %s started:" fname);
@@ -213,6 +254,7 @@ let main ~mode =
      begin
       HLog.error
        "there are still incomplete proofs at the end of the script";
+      pp_times fname bench_mode true big_bang;
       clean_exit (Some 2)
      end
     else
@@ -233,18 +275,23 @@ let main ~mode =
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
+       pp_times fname bench_mode true big_bang;
        exit 0
      end
   with 
   | Sys.Break ->
       HLog.error "user break!";
+      pp_times fname bench_mode false big_bang;
       if mode = `COMPILER then
         clean_exit (Some ~-1)
       else
         pp_ocaml_mode ()
   | GrafiteEngine.Drop ->
       if mode = `COMPILER then 
-        clean_exit (Some 1)
+        begin
+          pp_times fname bench_mode false big_bang;
+          clean_exit (Some 1)
+        end
       else 
         pp_ocaml_mode ()
   | GrafiteEngine.Macro (floc,_) ->
@@ -252,20 +299,29 @@ let main ~mode =
       HLog.error
        (sprintf "A macro has been found in a script at %d-%d" x y);
       if mode = `COMPILER then 
-        clean_exit (Some 1)
+        begin
+          pp_times fname bench_mode false big_bang;
+          clean_exit (Some 1)
+        end
       else 
         pp_ocaml_mode ()
   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
      let (x, y) = HExtlib.loc_of_floc floc in
      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      if mode = `COMPILER then
-       clean_exit (Some 1)
+       begin
+         pp_times fname bench_mode false big_bang;
+         clean_exit (Some 1)
+       end
      else
        pp_ocaml_mode ()
   | exn ->
       if matita_debug then raise exn;
       if mode = `COMPILER then 
-        clean_exit (Some 3)
+        begin
+          pp_times fname bench_mode false big_bang;
+          clean_exit (Some 3)
+        end
       else 
         pp_ocaml_mode ()