X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=f56ba5840cda99a19b44ea95d38e9a57b7b3a5a1;hb=f620bf94af6c347926ed1c2328462efab7018b21;hp=da51369348d16ccb71c4894a477841f12fbe7b57;hpb=85b400c16c933f6ee791f5d2783f466836651a3c;p=helm.git diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index da5136934..f56ba5840 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -1,5 +1,37 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + let debug = false;; +let timestamp msg = + if debug then + let times = Unix.times () in + let utime = times.Unix.tms_utime in + let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg utime in + prerr_endline msg + exception NoRootFor of string let absolutize path = @@ -40,7 +72,10 @@ let remove_trailing_slash s = let load_root_file rootpath = let data = HExtlib.input_file rootpath in let lines = Str.split (Str.regexp "\n") data in - let clean s = Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s) in + let clean s = + Pcre.replace ~pat:"[ \t]+" ~templ:" " + (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s)) + in List.map (fun l -> match Str.split (Str.regexp "=") l with @@ -49,7 +84,7 @@ let load_root_file rootpath = lines ;; -let find_root_for ~include_paths file = +let rec find_root_for ~include_paths file = let include_paths = "" :: Sys.getcwd () :: include_paths in try let path = HExtlib.find_in include_paths file in @@ -73,10 +108,16 @@ let find_root_for ~include_paths file = HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path with Failure "find_in" -> - HLog.error ("We are in: " ^ Sys.getcwd ()); - HLog.error ("Unable to find: "^file^"\nPaths explored:"); - List.iter (fun x -> HLog.error (" - "^x)) include_paths; - raise (NoRootFor file) + if Filename.check_suffix file ".ma" then begin + let mma = Filename.chop_suffix file ".ma" ^ ".mma" in + HLog.warn ("We look for: " ^ mma); + find_root_for ~include_paths mma + end else begin + HLog.error ("We are in: " ^ Sys.getcwd ()); + HLog.error ("Unable to find: "^file^"\nPaths explored:"); + List.iter (fun x -> HLog.error (" - "^x)) include_paths; + raise (NoRootFor file) + end ;; let mk_baseuri root extra = @@ -154,11 +195,16 @@ module type Format = module Make = functor (F:Format) -> struct + type status = Done of bool + | Ready of bool + let say s = if debug then prerr_endline ("make: "^s);; let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; - let younger_s_t (_,cs,ct) a b = + let fst4 = function (x,_,_,_) -> x;; + + let younger_s_t (_,cs, ct, _, _) a b = let a = try Hashtbl.find cs a with Not_found -> assert false in let b = try @@ -177,7 +223,7 @@ module Make = functor (F:Format) -> struct | _ -> false ;; - let younger_t_t (_,_,ct) a b = + let younger_t_t (_,_,ct, _, _) a b = let a = try match Hashtbl.find ct a with @@ -207,72 +253,6 @@ module Make = functor (F:Format) -> struct | _ -> false ;; - let is_built opts t tgt = - younger_s_t opts t tgt - ;; - - let assoc4 l k = List.find (fun (k1,_,_,_) -> k1 = k) l;; - - let fst4 = function (x,_,_,_) -> x;; - - let rec needs_build opts deps compiled (t,dependencies,root,tgt) = - say ("Checking if "^F.string_of_source_object t^ " needs to be built"); - if List.mem t compiled then - (say "already compiled"; false) - else - if not (is_built opts t tgt) then - (say(F.string_of_source_object t^" is not built, thus needs to be built"); - true) - else - try - let unsat = - List.find - (needs_build opts deps compiled) - (List.map (assoc4 deps) dependencies) - in - say (F.string_of_source_object t^" depends on "^ - F.string_of_source_object (fst4 unsat)^ - " that needs to be built, thus needs to be built"); - true - with Not_found -> - try - let _,_,_,unsat = - List.find - (fun (_,_,_,tgt1) -> younger_t_t opts tgt tgt1) - (List.map (assoc4 deps) dependencies) - in - say - (F.string_of_source_object t^" depends on "^F.string_of_target_object - unsat^" and "^F.string_of_source_object t^".o is younger than "^ - F.string_of_target_object unsat^", thus needs to be built"); - true - with Not_found -> false - ;; - - let is_buildable opts compiled deps (t,dependencies,root,tgt as what) = - say ("Checking if "^F.string_of_source_object t^" is buildable"); - let b = needs_build opts deps compiled what in - if not b then - (say (F.string_of_source_object t^ - " does not need to be built, thus it not buildable"); - false) - else - try - let unsat,_,_,_ = - List.find (needs_build opts deps compiled) - (List.map (assoc4 deps) dependencies) - in - say (F.string_of_source_object t^" depends on "^ - F.string_of_source_object unsat^ - " that needs build, thus is not buildable"); - false - with Not_found -> - say - ("None of "^F.string_of_source_object t^ - " dependencies needs to be built, thus it is buildable"); - true - ;; - let rec purge_unwanted_roots wanted deps = let roots, rest = List.partition @@ -287,15 +267,62 @@ module Make = functor (F:Format) -> struct purge_unwanted_roots wanted (newroots @ rest) ;; - let is_not_ro (opts,_,_) (f,_,r,_) = + let is_not_ro (opts,_,_,_,_) (f,_,r,_) = match r with | Some root -> not (F.is_readonly_buri_of opts f) | None -> assert false ;; - let rec make_aux root (lo,_,ct as opts) compiled failed deps = - let todo = List.filter (is_buildable opts compiled deps) deps in - let todo = List.filter (fun (f,_,_,_)->not (List.mem f failed)) todo in + let rec get_status opts what = + let _, _, _, cc, cd = opts in + let t, dependencies, root, tgt = what in + try Done (Hashtbl.find cc t) +(* say "already built" *) + with Not_found -> + let map st d = match st with + | Done false -> st + | Ready false -> st + | _ -> + let whatd = Hashtbl.find cd d in + let _, _, _, tgtd = whatd in + begin match st, get_status opts whatd with + | _, Done false -> Hashtbl.add cc t false; Done false + | Done true, Done true -> + if younger_t_t opts tgt tgtd then Ready true else Done true +(* say (F.string_of_source_object t^" depends on "^F.string_of_target_object unsat^" and "^F.string_of_source_object t^".o is younger than "^ F.string_of_target_object unsat^", thus needs to be built") *) + | Done true, Ready _ -> Ready false + | Ready true, Ready _ -> Ready false +(* say (F.string_of_source_object t^" depends on "^ F.string_of_source_object (fst4 unsat)^ " that is not built, thus is not ready") *) + | Ready true, Done true -> Ready true + | _ -> st + end + in + let st = if younger_s_t opts t tgt then Done true else Ready true in + match List.fold_left map st dependencies with + | Done true -> Hashtbl.add cc t true; Done true +(* say(F.string_of_source_object t^" is built" *) + | st -> st + + let list_partition_filter_rev filter l = + let rec aux l1 l2 = function + | [] -> l1, l2 + | hd :: tl -> + begin match filter hd with + | None -> aux l1 l2 tl + | Some true -> aux (hd :: l1) l2 tl + | Some false -> aux l1 (hd :: l2) tl + end + in + aux [] [] l + + let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps = + timestamp "filter get_status: begin"; + let map what = match get_status opts what with + | Done _ -> None + | Ready b -> Some b + in + let todo, deps = list_partition_filter_rev map deps in + timestamp "filter get_status: end"; let todo = let local, remote = List.partition (fun (_,_,froot,_) -> froot = Some root) todo @@ -307,36 +334,42 @@ module Make = functor (F:Format) -> struct skipped; remote @ local in - if todo <> [] then - let compiled, failed = - List.fold_left - (fun (c,f) (file,_,froot,tgt) -> + if todo <> [] then begin + let ok = List.fold_left + (fun ok (file,_,froot,tgt) -> let rc = match froot with | Some froot when froot = root -> Hashtbl.remove ct tgt; Hashtbl.add ct tgt None; - F.build lo file + timestamp "building"; + let r = F.build lo file in + timestamp "done"; r | Some froot -> make froot [file] | None -> HLog.error ("No root for: "^F.string_of_source_object file); false in - if rc then (file::c,f) - else (c,file::f)) - (compiled,failed) todo - in - make_aux root opts compiled failed deps + Hashtbl.add cc file rc; + ok && rc + ) + ok (List.rev todo) + in + make_aux root opts ok (List.rev deps) + end else - compiled, failed + ok and make root targets = + timestamp "entering"; HLog.debug ("Entering directory '"^root^"'"); let old_root = Sys.getcwd () in Sys.chdir root; let deps = F.load_deps_file (root^"/depends") in let local_options = load_root_file (root^"/root") in - let caches,cachet = Hashtbl.create 73, Hashtbl.create 73 in + let caches,cachet,cachec,cached = + Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 + in (* deps are enriched with these informations to sped up things later *) let deps = List.map @@ -344,29 +377,40 @@ module Make = functor (F:Format) -> struct let r,tgt = F.root_and_target_of local_options file in Hashtbl.add caches file (F.mtime_of_source_object file); Hashtbl.add cachet tgt (F.mtime_of_target_object tgt); - file, d, r, tgt) + Hashtbl.add cached file (file, d, r, tgt); + (file, d, r, tgt) + ) deps in - let opts = local_options, caches, cachet in - let _compiled, failed = + let opts = local_options, caches, cachet, cachec, cached in + let ok = if targets = [] then - make_aux root opts [] [] deps + make_aux root opts true deps else - make_aux root opts [] [] (purge_unwanted_roots targets deps) + make_aux root opts true + (purge_unwanted_roots targets deps) in HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; - failed = [] + timestamp "leaving"; + ok ;; end -let write_deps_file root deps = - let oc = open_out (root ^ "/depends") in - List.iter - (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) - deps; - close_out oc; - HLog.message ("Generated: " ^ root ^ "/depends") -;; - +let write_deps_file where deps = match where with + | Some root -> + let oc = open_out (root ^ "/depends") in + let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in + List.iter map deps; close_out oc; + HLog.message ("Generated: " ^ root ^ "/depends") + | None -> + print_endline (String.concat " " (List.flatten (List.map snd deps))) + +(* FG ***********************************************************************) + +(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) +let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:" + +let is_uri str = + Pcre.pmatch ~rex:uri_scheme_rex str