X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=fc64479f12fd8fce2e896a628028cf7c9a597b05;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=ec5618684426cf9607b7e94fc31a3f8eb00f50db;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index ec5618684..fc64479f1 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -64,10 +64,12 @@ let get_macro_context = function | 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 "OK","Ok" else "FAIL","Fail" in @@ -107,11 +109,28 @@ let get_include_paths options = 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:[] @@ -119,6 +138,9 @@ let compile options fname = 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 *) @@ -129,9 +151,6 @@ let compile options fname = 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 <> []) @@ -139,16 +158,7 @@ let compile options fname = HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); LibraryClean.clean_baseuris [baseuri]; - assert (Http_getter_storage.is_empty ~local:true 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 = @@ -158,6 +168,16 @@ let compile options fname = 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 _ _ -> ()) @@ -196,7 +216,7 @@ let compile options fname = 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) @@ -217,14 +237,14 @@ let compile options fname = 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 @@ -236,18 +256,18 @@ let compile options fname = 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 ;; @@ -258,6 +278,11 @@ module F = 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