}
let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
{ do_it =
fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.CicUtil.profile
+ -> profiler.HExtlib.profile
(disambiguate_thing ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff) thing
}
with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
;;
-let profiler_include = CicUtil.profile "include"
+let profiler_include = HExtlib.profile "include"
let eval_command opts status cmd =
let status,cmd = disambiguate_command status cmd in
raise (IncludedFileNotCompiled moopath) in
let stream = Ulexing.from_utf8_channel ic in
let status = ref status in
- profiler_include.CicUtil.profile
+ profiler_include.HExtlib.profile
(!eval_from_stream_ref status stream) (fun _ _ -> ());
close_in ic;
!status
status.aliases []
let alias_diff =
- let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
let set_proof_aliases status new_aliases =
let aliases =
| _-> assert false)
let typecheck_obj =
- let profiler = CicUtil.profile "add_obj.typecheck_obj" in
- fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
+ let profiler = HExtlib.profile "add_obj.typecheck_obj" in
+ fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
let index_obj =
- let profiler = CicUtil.profile "add_obj.index_obj" in
+ let profiler = HExtlib.profile "add_obj.index_obj" in
fun ~dbd ~uri ->
- profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-
-let save_object_to_disk =
- let profiler = CicUtil.profile "add_obj.save_object_to_disk" in
- fun status uri obj ugraph univlist ->
- profiler.CicUtil.profile (save_object_to_disk status uri obj ugraph) univlist
+ profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
let add_obj uri obj status =
let dbd = MatitaDb.instance () in
end
let add_obj =
- let profiler = CicUtil.profile "add_obj" in
- fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
+ let profiler = HExtlib.profile "add_obj" in
+ fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
module OrderedUri =
struct