module HG = Http_getter;;
module UM = UriManager;;
-let cache_of_processed_baseuri = Hashtbl.create 1024
-let one_step_depend suri =
- let buri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with UM.IllFormedUri _ -> suri
- in
+let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;;
+
+let safe_buri_of_suri suri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with
+ UM.IllFormedUri _ -> suri
+
+let one_step_depend cache_of_processed_baseuri suri dbtype dbd =
+ let buri = safe_buri_of_suri suri in
if Hashtbl.mem cache_of_processed_baseuri buri then
[]
else
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
- sprintf ("SELECT source, h_occurrence FROM %s WHERE "
- ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
- else
- begin
- HLog.debug "Warning SELECT without REGEXP";
- sprintf
- ("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence LIKE '%s%%'")
- obj_tbl buri
- end
+ if HSql.isMysql dbtype dbd then
+ sprintf ("SELECT source, h_occurrence FROM %s WHERE "
+ ^^ "h_occurrence REGEXP '"^^
+ "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'")
+ obj_tbl buri
+ else
+ begin
+ sprintf ("SELECT source, h_occurrence FROM %s WHERE "
+ ^^ "REGEXP(h_occurrence, '"^^
+ "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')")
+ obj_tbl buri
+ (* implementation with vanilla ocaml-sqlite3
+ HLog.debug "Warning SELECT without REGEXP";
+ sprintf
+ ("SELECT source, h_occurrence FROM %s WHERE " ^^
+ "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like)
+ obj_tbl buri*)
+ 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 ->
match row.(0), row.(1) with
- | Some uri, Some occ when Filename.dirname occ = buri ->
- l := uri :: !l
+ | Some uri, Some occ when
+ Filename.dirname (strip_xpointer occ) = buri ->
+ l := uri :: !l
| _ -> ());
let l = List.sort Pervasives.compare !l in
HExtlib.list_uniq l
exn -> raise exn (* no errors should be accepted *)
end
-let safe_buri_of_suri suri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with
- 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
+ ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri
else
begin
- HLog.debug "Warning SELECT without REGEXP";
- sprintf
- ("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence LIKE '%s%%'")
- obj_tbl buri
+ sprintf ("SELECT source FROM %s WHERE "
+ ^^ "REGEXP(source, '^%s[^/]*\\(#xpointer.*\\)?$')") obj_tbl buri
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 ->
match row.(0) with
- | Some uri when Filename.dirname uri = buri ->
+ | Some uri when Filename.dirname (strip_xpointer uri) = buri ->
l := uri :: !l
| _ -> ());
let l = List.sort Pervasives.compare !l in
exn -> raise exn (* no errors should be accepted *)
;;
-let close_uri_list uri_to_remove =
+let close_uri_list cache_of_processed_baseuri 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
in
let uri_to_remove_from_db =
List.fold_left
- (fun acc buri -> db_uris_of_baseuri buri @ acc
+ (fun acc buri ->
+ let dbu = db_uris_of_baseuri buri in
+ dbu @ acc
) [] buri_to_remove
in
let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
(* 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 cache_of_processed_baseuri u dbtype dbd @ acc)
+ [] uri_to_remove
in
let depend =
HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
in
uri_to_remove, depend
+;;
-let rec close_db uris next =
+let rec close_db cache_of_processed_baseuri uris next =
match next with
| [] -> uris
- | l -> let uris, next = close_uri_list l in close_db uris next @ uris
+ | l ->
+ let uris, next = close_uri_list cache_of_processed_baseuri l in
+ close_db cache_of_processed_baseuri uris next @ uris
+;;
let cleaned_no = ref 0;;
| _ -> assert false)
(Helm_registry.get_list Helm_registry.string "getter.prefix"))
in
- 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
+ String.sub url 7 (String.length url - 7))
+;;
let clean_baseuris ?(verbose=true) buris =
+ let cache_of_processed_baseuri = Hashtbl.create 1024 in
+ 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 cache_of_processed_baseuri [] 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) ;
let buri = UriManager.buri_of_uri uri in
if buri <> !last_baseuri then
begin
- if Helm_registry.get_bool "matita.bench" then
+ if not (Helm_registry.get_bool "matita.verbose") then
(print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
else
HLog.message ("Removing: " ^ buri ^ "/*");
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