+ (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
+ | AttemptToInsertAnAlias lexicon_status ->
+ 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
+ | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
+ (match exn with
+ | Sys.Break -> HLog.error "user break!"
+ | 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)
+ | exn when matita_debug -> raise exn'
+ | exn -> HLog.error (snd (MatitaExcPp.to_string exn))
+ );
+(* LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
+ * *)
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+ | Sys.Break when not matita_debug ->
+ HLog.error "user break!";
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+ | exn when not matita_debug ->
+ HLog.error
+ ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+
+module F =
+ struct
+ type source_object = string
+ type target_object = string
+ 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
+ let root,baseuri,_,relpath =
+ Librarian.baseuri_of_script ~include_paths mafile
+ in
+ let obj_writeable, obj_read_only =
+ if Filename.check_suffix mafile ".mma" then
+ Filename.chop_suffix mafile ".mma" ^ ".ma",
+ Filename.chop_suffix mafile ".mma" ^ ".ma"
+ else
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ Some root, relpath, obj_writeable, obj_read_only
+ with Librarian.NoRootFor x -> None, "", "", ""
+ ;;
+
+ let mtime_of_source_object s =
+ try Some (Unix.stat s).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+ ;;
+
+ let mtime_of_target_object s =
+ try Some (Unix.stat s).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+ ;;
+
+(* FG: a problem was noticed in relising memory between subsequent *)
+(* invocations of the compiler. The following might help *)
+ let compact r = Gc.compact (); r
+
+ let build options fname =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let compile atstart opts fname =
+ try
+ GrafiteSync.push ();
+ GrafiteParser.push ();
+ let rc = compile atstart opts fname in
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ rc
+ with
+ | Sys.Break ->
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ false
+ | exn when not matita_debug ->
+ HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
+ assert false
+ in
+ if Filename.check_suffix fname ".mma" then
+ let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
+ let atstart, atexit = dump generated in
+ let res = compile atstart options fname in
+ let r = compact (atexit res) in
+ if r then r else begin
+(* Sys.remove generated; *)
+ Printf.printf "rm %s\n" generated; flush stdout; r
+ end