let magic = 2;;
+let prerr_endline _ = ()
+
let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
let refresh_uri_in_universe =
let path = String.sub uri 4 (String.length uri - 4) in
let path = match user with
| Some u -> "/" ^ u ^ path
- | _ -> path
+ | _ -> prerr_endline "WARNING: ng_path_of_baseuri called without a uid"; path
in
let path = Helm_registry.get "matita.basedir" ^ path in
let dirname = Filename.dirname path in
let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
-let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+let db_path user =
+ let midpath = match user with
+ | None -> ""
+ | Some u -> "/" ^ u
+ in
+ Helm_registry.get "matita.basedir" ^ midpath ^ "/ng_db.ng";;
type timestamp =
[ `Obj of NUri.uri * NCic.obj
let time0 = [],[];;
+let global_aliases_db = ref [];;
+let rev_includes_map_db = ref [];;
+
+let global_aliases u =
+ try List.assoc u !global_aliases_db
+ with Not_found ->
+ let db = ref [] in
+ global_aliases_db := (u,db)::!global_aliases_db;
+ db
+;;
+
+let rev_includes_map u =
+ try List.assoc u !rev_includes_map_db
+ with Not_found ->
+ let db = ref NUri.UriMap.empty in
+ rev_includes_map_db := (u,db)::!rev_includes_map_db;
+ db
+;;
+
let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
- let global_aliases = ref [] in
- let rev_includes_map = ref NUri.UriMap.empty in
- let store_db () =
- let ch = open_out (db_path ()) in
- Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
+ let store_db user =
+ let ch = open_out (db_path user) in
+ Marshal.to_channel ch (magic,(!(global_aliases user),!(rev_includes_map user))) [];
close_out ch in
- let load_db () =
+ let load_db user =
HExtlib.mkdir (Helm_registry.get "matita.basedir");
+ if user <> None then HExtlib.mkdir ((Helm_registry.get "matita.basedir") ^ "/" ^ HExtlib.unopt user);
try
- let ga,im = require_path (db_path ()) in
+ let ga,im = require_path (db_path user) in
let ga =
List.map
(fun (uri,name,NReference.Ref (uri2,spec)) ->
(fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
) im NUri.UriMap.empty
in
- global_aliases := ga;
- rev_includes_map := im
+ global_aliases user := ga;
+ rev_includes_map user := im
with
Sys_error _ -> () in
- let get_deps u =
+ let get_deps user u =
let get_deps_one_step u =
- try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+ try NUri.UriMap.find u !(rev_includes_map user) with Not_found -> [] in
let rec aux res =
function
[] -> res
aux (he::res) (get_deps_one_step he @ tl)
in
aux [] [u] in
- let remove_deps u =
- rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
- rev_includes_map :=
+ let remove_deps user u =
+ rev_includes_map user := NUri.UriMap.remove u !(rev_includes_map user);
+ rev_includes_map user :=
NUri.UriMap.map
- (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
- store_db ()
+ (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !(rev_includes_map user);
+ store_db user
in
load_db,
- (fun ga -> global_aliases := ga; store_db ()),
- (fun () -> !global_aliases),
- (fun u l ->
- rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
- store_db ()),
+ (fun user ga -> global_aliases user := ga; store_db user),
+ (fun user -> !(global_aliases user)),
+ (fun user u l ->
+ rev_includes_map user := NUri.UriMap.add u (l @ get_deps user u) !(rev_includes_map user);
+ store_db user),
get_deps,
remove_deps
;;
val timestamp = (time0 : timestamp)
method timestamp = timestamp
+ method print_timestamp () =
+ prerr_endline ("length(lib_db.storage) = " ^
+ string_of_int (List.length !(lib_db.storage)));
+ prerr_endline ("length(timestamp.storage) = " ^
+ string_of_int (List.length (fst timestamp)));
method set_timestamp v = {< timestamp = v >}
method set_lib_db v = {< lib_db = v >}
method set_lib_status : 's.#g_status as 's -> 'self
;;
let time_travel0 st (sto,ali) =
+ prerr_endline ("length of lib_db.storage = " ^ (string_of_int (List.length !(st#lib_db.storage))));
+ prerr_endline ("length of sto = " ^ (string_of_int (List.length sto)));
let diff_len = List.length !(st#lib_db.storage) - List.length sto in
let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in
if List.length to_be_deleted > 0 then
end
module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
- val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s ->
- string option*) end) =
+ val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
+ string option end) =
struct
type dumpable_status = D.dumpable_s
type 'a register_type =
close_out ch
| `Constr _ -> ()
) !((D.get status)#lib_db.storage);
- set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ());
- List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
+ let user = D.user status in
+ set_global_aliases user (!((D.get status)#lib_db.local_aliases) @ get_global_aliases user);
+ List.iter (fun u -> add_deps (D.user status) u [baseuri]) (D.get status)#dump.includes;
reset_timestamp (D.get status)
let require2 ~baseuri ~alias_only status =
try
HExtlib.filter_map
(fun (_,name',nref) -> if name'=name then Some nref else None)
- (!(st#lib_db.local_aliases) @ get_global_aliases ())
+ (!(st#lib_db.local_aliases) @ get_global_aliases st#user)
with
- Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
+ Not_found ->
+ (prerr_endline ("can't resolve object " ^ name);
+ raise (NCicEnvironment.ObjectNotFound (lazy name)))
;;
let aliases_of st uri =
with Not_found ->*)
try fetch_obj (status#user) status u
with Sys_error _ ->
- raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
+ (prerr_endline ("can't fetch object " ^ NUri.string_of_uri u);
+ raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))))
;;
NCicEnvironment.set_get_obj