X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=7efad77212b3191d2d490253e8559f5e9e945385;hb=cea505df0c55c2bb6e239a0aba2abcf80550e920;hp=1297a47473839a8e4da1573374000538f5eef994;hpb=0fba218a0cad769861bda75d175f926f6e765640;p=helm.git diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 1297a4747..7efad7721 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -103,8 +103,7 @@ let clean_exit n = | Some grafite_status -> try let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in - let basedir = Helm_registry.get "matita.basedir" in - LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri]; + LibraryClean.clean_baseuris ~verbose:false [baseuri]; opt_exit n with GrafiteTypes.Option_error("baseuri", "not found") -> (* no baseuri ==> nothing to clean yet *) @@ -154,10 +153,55 @@ 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 "BENCH_EXTRA_TEXT" 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 fname = + match MatitamakeLib.development_for_dir (Filename.dirname fname) with + | None -> fname + | Some d -> + let rootlen = String.length(MatitamakeLib.root_for_development d)in + let fnamelen = String.length fname in + assert (fnamelen > rootlen); + String.sub fname rootlen (fnamelen - rootlen) + 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 ()); @@ -166,6 +210,7 @@ let main ~mode = BuildTimeConf.core_notation_script); Sys.catch_break true; let origcb = HLog.get_log_callback () in + let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in let newcb tag s = match tag with | `Debug | `Message -> () @@ -173,10 +218,11 @@ let main ~mode = in if Helm_registry.get_int "matita.verbosity" < 1 then HLog.set_log_callback newcb; + if bench_mode then MatitaMisc.shutup (); 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); @@ -212,35 +258,44 @@ 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 begin - let basedir = Helm_registry.get "matita.basedir" in let baseuri = DependenciesParser.baseuri_of_script ~include_paths fname in - let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in - let lexicon_fname= LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in + let moo_fname = + LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true + in + let lexicon_fname= + LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true + in let metadata_fname = - LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri + LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in GrafiteMarshal.save_moo moo_fname moo_content_rev; LibraryNoDb.save_metadata metadata_fname metadata; 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,_) -> @@ -248,20 +303,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 ()