From: Enrico Tassi Date: Wed, 15 Mar 2006 11:27:02 +0000 (+0000) Subject: snapshot for release X-Git-Tag: make_still_working~7508 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=64afac782fe3bd83dbc2f9295481362f1edc8e68;p=helm.git snapshot for release --- diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index ffa2c8ef9..bb341d245 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/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/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 06f7815b9..f66ec6aff 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/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/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 8135e2472..ca587690c 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/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 ()