+ loop asserted status str
+
+and compile ~compiling ~asserted ~include_paths fname =
+ if List.mem fname compiling then raise (CircularDependency fname);
+ let compiling = fname::compiling in
+ let matita_debug = Helm_registry.get_bool "matita.debug" 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;
+ (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
+ let status = new status baseuri in
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
+ let ocamldirname = Filename.dirname fname in
+ let ocamlfname = Filename.chop_extension (Filename.basename fname) in
+ let status,ocamlfname =
+ Common.modname_of_filename status false ocamlfname in
+ let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
+ let status = OcamlExtraction.open_file status ~baseuri ocamlfname 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
+ let cc =
+ let rex = Str.regexp ".*opt$" in
+ if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
+ else "matitac" in
+ let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in
+ try
+ (* cleanup of previously compiled objects *)
+ if (not (Http_getter_storage.is_empty ~local:true baseuri))
+ then begin
+ HLog.message ("baseuri " ^ baseuri ^ " is not empty");
+ HLog.message ("cleaning baseuri " ^ baseuri);
+ LibraryClean.clean_baseuris [baseuri];
+ end;
+ HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
+ if not (Helm_registry.get_bool "matita.verbose") then
+ (print_string true (s ^ "\n"); 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 =
+ GrafiteParser.parsable_statement status
+ (Ulexing.from_utf8_channel (open_in fname))
+ in
+ let print_cb =
+ if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
+ else pp_ast_statement
+ in
+ let asserted, status =
+ eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+ let status = OcamlExtraction.close_file status in
+ let elapsed = Unix.time () -. time in
+ (if Helm_registry.get_bool "matita.moo" then begin
+ GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ status
+ end;
+ let tm = Unix.gmtime elapsed in
+ let sec = string_of_int tm.Unix.tm_sec ^ "''" in
+ let min =
+ if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
+ in
+ let hou =
+ if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else ""
+ in
+ HLog.message
+ (sprintf "execution of %s completed in %s." fname (hou^min^sec));
+ pp_times s fname true big_bang big_bang_u big_bang_s;
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
+(* MATITA 1.0: debbo fare time_travel sulla ng_library?
+ LexiconSync.time_travel
+ ~present:lexicon_status ~past:initial_lexicon_status;
+*)
+ asserted)
+ with
+ (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
+ | exn when not matita_debug ->
+(* MATITA 1.0: debbo fare time_travel sulla ng_library?
+ LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
+ * *)
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
+ pp_times s fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri exn
+
+and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
+ let root,baseuri,fullmapath,_ =
+ Librarian.baseuri_of_script ~include_paths mapath in
+ if List.mem fullmapath asserted then asserted,false
+ else
+ begin
+ let include_paths =
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ root::includes @
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let baseuri = NUri.uri_of_string baseuri in
+ let ngtime_of baseuri =
+ let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ try
+ Some (Unix.stat ngpath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
+ let matime =
+ try (Unix.stat fullmapath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
+ in
+ let ngtime = ngtime_of baseuri in
+ let asserted,to_be_compiled =
+ match ngtime with
+ Some ngtime ->
+ let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let asserted,children_bad =
+ List.fold_left
+ (fun (asserted,b) mapath ->
+ let asserted,b1 =
+ try
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mapath
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ asserted, true
+ in
+ asserted, b || b1
+ || let _,baseuri,_,_ =
+ (*CSC: bug here? include_paths should be empty and
+ mapath should be absolute *)
+ Librarian.baseuri_of_script ~include_paths mapath in
+ let baseuri = NUri.uri_of_string baseuri in
+ (match ngtime_of baseuri with
+ Some child_ngtime -> child_ngtime > ngtime
+ | None -> assert false)
+ ) (asserted,false) preamble
+ in
+ asserted, children_bad || matime > ngtime
+ | None -> asserted,true
+ in
+ if not to_be_compiled then fullmapath::asserted,false
+ else
+ if List.mem baseuri already_included then
+ (* maybe recompiling it I would get the same... *)
+ raise (AlreadyLoaded (lazy mapath))
+ else
+ let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+ fullmapath::asserted,true
+ end