let cache_of_processed_baseuri = Hashtbl.create 1024
-let one_step_depend suri =
+let one_step_depend suri dbtype dbd =
let buri =
try
UM.buri_of_uri (UM.uri_of_string suri)
Hashtbl.add cache_of_processed_baseuri buri true;
let query =
let buri = buri ^ "/" in
- let buri = HSql.escape buri in
+ let buri = HSql.escape dbtype dbd buri in
let obj_tbl = MetadataTypes.obj_tbl () in
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
sprintf ("SELECT source, h_occurrence FROM %s WHERE "
^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
else
end
in
try
- let rc = HSql.exec (LibraryDb.instance ()) query in
+ let rc = HSql.exec dbtype dbd query in
let l = ref [] in
HSql.iter rc (
fun row ->
UM.IllFormedUri _ -> suri
let db_uris_of_baseuri buri =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let query =
let buri = buri ^ "/" in
- let buri = HSql.escape buri in
+ let buri = HSql.escape dbtype dbd buri in
let obj_tbl = MetadataTypes.name_tbl () in
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
sprintf ("SELECT source FROM %s WHERE "
^^ "source REGEXP '^%s[^/]*$'") obj_tbl buri
else
end
in
try
- let rc = HSql.exec (LibraryDb.instance ()) query in
+ let rc = HSql.exec dbtype dbd query in
let l = ref [] in
HSql.iter rc (
fun row ->
;;
let close_uri_list uri_to_remove =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
(* to remove an uri you have to remove the whole script *)
let buri_to_remove =
HExtlib.list_uniq
try
List.fold_left
(fun acc buri ->
- let inhabitants = HG.ls (buri ^ "/") in
+ let inhabitants = HG.ls ~local:true (buri ^ "/") in
let inhabitants = List.filter
(function HGT.Ls_object _ -> true | _ -> false)
inhabitants
(* now we want the list of all uri that depend on them *)
let depend =
List.fold_left
- (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
+ (fun acc u -> one_step_depend u dbtype dbd @ acc) [] uri_to_remove
in
let depend =
HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
)
-let close_nodb buris =
- let rev_deps = Hashtbl.create 97 in
- let all_metadata =
- HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
- (Lazy.force moo_root_dir)
- in
- List.iter
- (fun path ->
- let metadata = LibraryNoDb.load_metadata ~fname:path in
- let baseuri_of_current_metadata =
- prerr_endline "ERROR, add to the getter reverse lookup";
- let basedir = "/fake" in
- let dirname = Filename.dirname path in
- let basedirlen = String.length basedir in
- assert (String.sub dirname 0 basedirlen = basedir);
- "cic:" ^
- String.sub dirname basedirlen (String.length dirname - basedirlen) ^
- Filename.basename path
- in
- let deps =
- HExtlib.filter_map
- (function LibraryNoDb.Dependency buri -> Some buri)
- metadata
- in
- List.iter
- (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps)
- all_metadata;
- let buris_to_remove =
- HExtlib.list_uniq
- (List.fast_sort Pervasives.compare
- (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
- in
- let objects_to_remove =
- let objs_of_buri buri =
- HExtlib.filter_map
- (function
- | Http_getter_types.Ls_object o ->
- Some (buri ^ "/" ^ o.Http_getter_types.uri)
- | _ -> None)
- (Http_getter.ls buri)
- in
- List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
- in
- objects_to_remove
-
let clean_baseuris ?(verbose=true) buris =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
Hashtbl.clear cache_of_processed_baseuri;
let buris = List.map Http_getter_misc.strip_trailing_slash buris in
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
- let l =
- if Helm_registry.get_bool "db.nodb" then
- close_nodb buris
- else
- close_db [] buris
- in
+ let l = close_db [] buris in
let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
let l = List.map UriManager.uri_of_string l in
debug_prerr "clean_baseuri will remove:";
LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
in
HExtlib.safe_remove obj_file ;
- HExtlib.safe_remove
- (LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~writable:true ~baseuri) ;
HExtlib.safe_remove
(LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~writable:true ~baseuri) ;
end;
LibrarySync.remove_obj uri
) l;
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
begin
cleaned_no := !cleaned_no + List.length l;
- if !cleaned_no > 30 then
+ if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
begin
cleaned_no := 0;
List.iter
(function table ->
- ignore (HSql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
[MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
MetadataTypes.count_tbl()]
projects / helm.git / blobdiff