* http://helm.cs.unibo.it/
*)
+open Printf
+
let debug = false
let debug_prerr = if debug then prerr_endline else ignore
module UM = UriManager;;
module TA = GrafiteAst;;
-let baseuri_of_baseuri_decl st =
- match st with
- | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
- Some buri
- | _ -> None
-
let cache_of_processed_baseuri = Hashtbl.create 1024
let one_step_depend suri =
Hashtbl.add cache_of_processed_baseuri buri true;
let query =
let buri = buri ^ "/" in
- let buri = Mysql.escape buri in
+ let buri = HMysql.escape buri in
let obj_tbl = MetadataTypes.obj_tbl () in
- Printf.sprintf
- "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+ sprintf
+ ("SELECT source, h_occurrence FROM %s WHERE " ^^
+ "h_occurrence REGEXP '^%s[^/]*$'")
+ obj_tbl buri
in
try
- let rc = Mysql.exec (MatitaDb.instance ()) query in
+ let rc = HMysql.exec (MatitaDb.instance ()) query in
let l = ref [] in
- Mysql.iter rc (
+ HMysql.iter rc (
fun row ->
match row.(0), row.(1) with
| Some uri, Some occ when Filename.dirname occ = buri ->
l := uri :: !l
| _ -> ());
let l = List.sort Pervasives.compare !l in
- MatitaMisc.list_uniq l
+ HExtlib.list_uniq l
with
exn -> raise exn (* no errors should be accepted *)
end
-
let safe_buri_of_suri suri =
try
let close_uri_list uri_to_remove =
(* to remove an uri you have to remove the whole script *)
let buri_to_remove =
- MatitaMisc.list_uniq
+ HExtlib.list_uniq
(List.fast_sort Pervasives.compare
(List.map safe_buri_of_suri uri_to_remove))
in
(fun acc u -> one_step_depend u @ acc) [] uri_to_remove
in
let depend =
- MatitaMisc.list_uniq
- (List.fast_sort Pervasives.compare depend)
+ HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
in
uri_to_remove, depend
-let baseuri_of_file file =
- let uri = ref None in
- let ic = open_in file in
- let istream = Stream.of_channel ic in
- (try
- while true do
- let stm = GrafiteParser.parse_statement istream in
- match baseuri_of_baseuri_decl stm with
- | Some buri ->
- let u = MatitaMisc.strip_trailing_slash buri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
- (try
- ignore(HG.resolve u)
- with
- | HGT.Unresolvable_URI _ ->
- MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
- | HGT.Key_not_found _ -> ());
- uri := Some u;
- raise End_of_file
- | None -> ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
-
-let rec fix uris next =
+let rec close_using_db uris next =
match next with
| [] -> uris
- | l -> let uris, next = close_uri_list l in fix uris next @ uris
+ | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
+let cleaned_no = ref 0;;
+
+ (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+ let url =
+ List.assoc "cic:/matita/"
+ (List.map
+ (fun pair ->
+ match
+ Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+ with
+ | [a;b] -> a, b
+ | _ -> 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_using_moos buris =
+ let rev_deps = Hashtbl.create 97 in
+ let all_moos =
+ HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+ (Lazy.force moo_root_dir)
+ in
+ List.iter
+ (fun path ->
+ let _, metadata = MatitaMoo.load_moo ~fname:path in
+ let baseuri_of_current_moo =
+ let rec aux = function
+ | [] -> assert false
+ | GrafiteAst.Baseuri buri::_ -> buri
+ | _ :: tl -> aux tl
+ in
+ aux metadata
+ in
+ let deps =
+ HExtlib.filter_map
+ (function
+ | GrafiteAst.Dependency buri -> Some buri
+ | _ -> None )
+ metadata
+ in
+ List.iter
+ (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+ all_moos;
+ 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 =
Hashtbl.clear cache_of_processed_baseuri;
let buris = List.map HGM.strip_trailing_slash buris in
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
- let l = fix [] buris in
- let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
+ let l =
+ if Helm_registry.get_bool "db.nodb" then
+ close_using_moos buris
+ else
+ close_using_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:";
if debug then
List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
- List.iter (MatitaSync.remove ~verbose) l
-
-let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
+ List.iter
+ (fun buri ->
+ MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri))
+ (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+ (List.map (UriManager.buri_of_uri) l)));
+ List.iter (MatitaSync.remove ~verbose) l;
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ begin
+ cleaned_no := 0;
+ List.iter
+ (function table ->
+ ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+ MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+ MetadataTypes.count_tbl()]
+ end
+
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Ulexing.from_utf8_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match MatitaMisc.baseuri_of_baseuri_decl stm with
+ | Some buri ->
+ let u = MatitaMisc.strip_trailing_slash buri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+ MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri := Some u;
+ raise End_of_file
+ | None -> ()
+ with
+ CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ ()
+ done
+ with End_of_file -> close_in ic);
+ match !uri with
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+ let baseuri = baseuri_of_file f in
+ MatitaMisc.obj_file_of_baseuri baseuri
projects / helm.git / blobdiff