| None -> assert false
;;
-let pp_times fname rc big_bang =
+let pp_times fname rc big_bang big_bang_u big_bang_s =
if not (Helm_registry.get_bool "matita.verbose") then
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
+ let u = u -. big_bang_u in
+ let s = s -. big_bang_s in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
let rc,rcascii =
if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
include_paths
;;
+let activate_extraction baseuri fname =
+ if false then
+ let mangled_baseuri =
+ let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+ let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+ String.uncapitalize baseuri in
+ let f =
+ open_out
+ (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
+ LibrarySync.set_object_declaration_hook
+ (fun _ obj ->
+ output_string f (CicExportation.ppobj baseuri obj);
+ flush f);
+;;
+
let compile options fname =
let matita_debug = Helm_registry.get_bool "matita.debug" in
let include_paths = get_include_paths options in
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
+ activate_extraction baseuri fname ;
let grafite_status = GrafiteSync.init baseuri in
let lexicon_status =
CicNotation2.load_notation ~include_paths:[]
in
let initial_lexicon_status = lexicon_status in
let big_bang = Unix.gettimeofday () in
+ let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
+ Unix.times ()
+ in
let time = Unix.time () in
try
(* sanity checks *)
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
"there are still incomplete proofs at the end of the script";
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
clean_exit baseuri false)
in
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
- pp_times fname true big_bang;
+ pp_times fname true big_bang big_bang_u big_bang_s;
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
true)
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| AttemptToInsertAnAlias lexicon_status ->
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
clean_exit baseuri false
HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
| exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
| Sys.Break as exn ->
if matita_debug then raise exn;
HLog.error "user break!";
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
| exn ->
if matita_debug then raise exn;
HLog.error
("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
;;