| 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 *)
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- if Http_getter_storage.is_read_only baseuri then
- HLog.error
- (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
LibraryClean.db_uris_of_baseuri baseuri <> [])
then begin
HLog.message ("baseuri " ^ baseuri ^ " is not empty");
HLog.message ("cleaning baseuri " ^ baseuri);
- LibraryClean.clean_baseuris [baseuri]
+ LibraryClean.clean_baseuris [baseuri];
end;
- (* create dir for XML files *)
- if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
- ~default:false)
- then
- HExtlib.mkdir
- (Filename.dirname
- (Http_getter.filename ~local:true ~writable:true (baseuri ^
- "foo.con")));
HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
if not (Helm_registry.get_bool "matita.verbose") then
(let cc =
in
let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
print_string s; flush stdout);
+ (* we dalay this error check until we print 'matitac file ' *)
+ assert (Http_getter_storage.is_empty ~local:true baseuri);
+ (* create dir for XML files *)
+ if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+ ~default:false)
+ then
+ HExtlib.mkdir
+ (Filename.dirname
+ (Http_getter.filename ~local:true ~writable:true (baseuri ^
+ "foo.con")));
let buf = Ulexing.from_utf8_channel (open_in fname) in
let print_cb =
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
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
;;
let string_of_source_object s = s;;
let string_of_target_object s = s;;
+ let is_readonly_buri_of opts file =
+ let buri = List.assoc "baseuri" opts in
+ Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)
+ ;;
+
let root_and_target_of opts mafile =
try
let include_paths = get_include_paths opts in
projects / helm.git / blobdiff