X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=2c2ba6ff2fcc9394d461849ec2d51cce85791dd1;hb=1652681b5eb49332f1c78e6c26d3ae5c7253d382;hp=124b1a1f5a57ece6cb0260e213986709543b6231;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index 124b1a1f5..2c2ba6ff2 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -1,4 +1,40 @@ -let debug = false;; +(* 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 = ref 0 + +let time_stamp = + let old = ref 0.0 in + fun msg -> + if !debug > 0 then begin + let times = Unix.times () in + let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in + let lap = stamp -. !old in + Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr; + old := stamp + end exception NoRootFor of string @@ -40,7 +76,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 @@ -50,9 +89,23 @@ let load_root_file rootpath = ;; let find_root_for ~include_paths file = - let include_paths = "" :: Sys.getcwd () :: include_paths in - try - let path = HExtlib.find_in include_paths file in + let include_paths = "" :: Sys.getcwd () :: include_paths in + let rec find_path_for file = + try HExtlib.find_in include_paths file + with Failure "find_in" -> + if Filename.check_suffix file ".ma" then begin + let mma = Filename.chop_suffix file ".ma" ^ ".mma" in + HLog.warn ("We look for: " ^ mma); + let path = find_path_for mma in + Filename.chop_suffix path ".mma" ^ ".ma" + 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 + in + let path = find_path_for file in let path = absolutize path in (* HLog.debug ("file "^file^" resolved as "^path); *) let rootpath, root, buri = @@ -72,11 +125,17 @@ let find_root_for ~include_paths file = if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then 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) + +;; + +let mk_baseuri root extra = + let chop name = + assert(Filename.check_suffix name ".ma" || + Filename.check_suffix name ".mma"); + try Filename.chop_extension name + with Invalid_argument "Filename.chop_extension" -> name + in + remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra)) ;; let baseuri_of_script ~include_paths file = @@ -92,16 +151,9 @@ let baseuri_of_script ~include_paths file = | _ -> raise (NoRootFor (file ^" "^path^" "^root)) in let extra_buri = substract lpath lroot in - let chop name = - assert(Filename.check_suffix name ".ma" || - Filename.check_suffix name ".mma"); - try Filename.chop_extension name - with Invalid_argument "Filename.chop_extension" -> name - in let extra = String.concat "/" extra_buri in root, - remove_trailing_slash (HExtlib.normalize_path - (buri ^ "/" ^ chop extra)), + mk_baseuri buri extra, path, extra ;; @@ -143,184 +195,224 @@ module type Format = val string_of_target_object: target_object -> string val build: options -> source_object -> bool val root_and_target_of: - options -> source_object -> string option * target_object + options -> source_object -> + (* root, relative source, writeable target, read only target *) + string option * source_object * target_object * target_object val mtime_of_source_object: source_object -> float option val mtime_of_target_object: target_object -> float option + val is_readonly_buri_of: options -> source_object -> bool end module Make = functor (F:Format) -> struct - let prerr_endline s = if debug then prerr_endline ("make: "^s);; + type status = Done of bool + | Ready of bool + + let say s = if !debug > 0 then prerr_endline ("make: "^s);; let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; - let younger_s_t a fa b fb = - let a = unopt_or_call a F.mtime_of_source_object fa in - let b = unopt_or_call b F.mtime_of_target_object fb in - match a,b with - | Some a, Some b -> a < b - | _ -> false - ;; + let fst4 = function (x,_,_,_) -> x;; - let younger_t_t a fa b fb = - let a = unopt_or_call a F.mtime_of_target_object fa in - let b = unopt_or_call b F.mtime_of_target_object fb in - match a, b with - | Some a, Some b -> a < b - | _ -> false - ;; + let modified_before_s_t (_,cs, ct, _, _) a b = + + if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a); + if !debug > 1 then time_stamp ("L s_t: b " ^ F.string_of_target_object b); + + let a = try Hashtbl.find cs a with Not_found -> assert false in + let b = + try + match Hashtbl.find ct b with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object b with + | Some t as x -> + Hashtbl.remove ct b; + Hashtbl.add ct b x; x + | x -> x + with Not_found -> assert false + in + let r = match a, b with + | Some a, Some b -> a <= b + | _ -> false + in - let is_built opts mt t mtgt tgt = - younger_s_t mt t mtgt tgt - ;; + if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r); - let assoc6 l k = List.find (fun (k1,_,_,_,_,_) -> k1 = k) l;; + r - let fst6 = function (x,_,_,_,_,_) -> x;; + let modified_before_t_t (_,_,ct, _, _) a b = - let rec needs_build opts deps compiled (t,dependencies,root,tgt,mt,mtgt) = - prerr_endline ("Checking if "^F.string_of_source_object t^ - " needs to be built"); - if List.mem t compiled then - (prerr_endline "already compiled"; - false) - else - if not (is_built opts mt t mtgt tgt) then - (prerr_endline (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 (assoc6 deps) dependencies) - in - prerr_endline - (F.string_of_source_object t^" depends on "^ - F.string_of_source_object (fst6 unsat)^ - " that needs to be built, thus needs to be built"); - true - with Not_found -> - try - let _,_,_,unsat,_,_ = - List.find - (fun (_,_,_,tgt1,_,mtgt1) -> younger_t_t mtgt tgt mtgt1 tgt1) - (List.map (assoc6 deps) dependencies) - in - prerr_endline - (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 - ;; + if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a); + if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b); + + let a = + try + match Hashtbl.find ct a with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object a with + | Some t as x -> + Hashtbl.remove ct a; + Hashtbl.add ct a x; x + | x -> x + with Not_found -> assert false + in + let b = + try + match Hashtbl.find ct b with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object b with + | Some t as x -> + Hashtbl.remove ct b; + Hashtbl.add ct b x; x + | x -> x + with Not_found -> assert false + in + let r = match a, b with + | Some a, Some b -> - let is_buildable opts compiled deps (t,dependencies,root,tgt,_,_ as what) = - prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable"); - let b = needs_build opts deps compiled what in - if not b then - (prerr_endline (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 (assoc6 deps) dependencies) - in - prerr_endline - (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 -> - prerr_endline - ("None of "^F.string_of_source_object t^ - " dependencies needs to be built, thus it is buildable"); - true - ;; + if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a); + if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b); + + a <= b + | _ -> false + in + + if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r); + + r let rec purge_unwanted_roots wanted deps = let roots, rest = List.partition - (fun (t,d,_,_,_,_) -> - not (List.exists (fun (_,d1,_,_,_,_) -> List.mem t d1) deps)) + (fun (t,_,d,_,_) -> + not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps)) deps in - let newroots = List.filter (fun (t,_,_,_,_,_) -> List.mem t wanted) roots in + let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in if newroots = roots then deps else purge_unwanted_roots wanted (newroots @ rest) ;; + let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = + match r with + | Some root -> not (F.is_readonly_buri_of opts f) + | None -> assert false + ;; + +(* FG: new sorting algorithm ************************************************) - let rec make_aux root local_options compiled failed deps = - let todo = List.filter (is_buildable local_options compiled deps) deps in - let todo = List.filter (fun (f,_,_,_,_,_)->not (List.mem f failed)) todo in - if todo <> [] then - let compiled, failed = - let todo = - let local, remote = - List.partition (fun (_,_,froot,_,_,_) -> froot = Some root) todo + let rec make_aux root opts ok deps = + List.fold_left (make_one root opts) ok deps + + and make_one root opts ok what = + let lo, _, ct, cc, cd = opts in + let t, path, deps, froot, tgt = what in + let str = F.string_of_source_object t in + let map (okd, okt) d = + let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in + let r = make_one root opts okd whatd in + r, okt && modified_before_t_t opts tgtd tgt + in + time_stamp ("L : processing " ^ str); + try + let r = Hashtbl.find cc t in + time_stamp ("L : " ^ string_of_bool r ^ " " ^ str); + ok && r +(* say "already built" *) + with Not_found -> + let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in + let res = + if okd then + if okt then true else + let build path = match froot with + | Some froot when froot = root -> + if is_not_ro opts what then F.build lo path else + (HLog.error ("Read only baseuri for: " ^ str ^ + ", I won't compile it even if it is out of date"); + false) + | Some froot -> make froot [path] + | None -> HLog.error ("No root for: " ^ str); false in - remote @ local - in - List.fold_left - (fun (c,f) (file,_,froot,_,_,_) -> - let rc = - match froot with - | Some froot when froot = root -> - F.build local_options file - | 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 local_options compiled failed deps - else - compiled, failed + Hashtbl.remove ct tgt; + Hashtbl.add ct tgt None; + time_stamp ("L : BUILDING " ^ str); + let res = build path in + time_stamp ("L : DONE " ^ str); res + else false + in + time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); + Hashtbl.add cc t res; ok && res - and make root targets = +(****************************************************************************) + + and make root targets = + time_stamp "L : 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 baseuri = List.assoc "baseuri" local_options in + print_endline ("Entering HELM directory: " ^ baseuri); flush stdout; + 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 (fun (file,d) -> - HLog.debug (F.string_of_source_object file); - let r,tgt = F.root_and_target_of local_options file in - file, d, r, tgt, F.mtime_of_source_object file, - F.mtime_of_target_object tgt) + let r,path,wtgt,rotgt = F.root_and_target_of local_options file in + Hashtbl.add caches file (F.mtime_of_source_object file); + (* if a read only target exists, we use that one, otherwise + we use the writeable one that may be compiled *) + let _,_,_,_, tgt as tuple = + match F.mtime_of_target_object rotgt with + | Some _ as mtime -> + Hashtbl.add cachet rotgt mtime; + (file, path, d, r, rotgt) + | None -> + Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); + (file, path, d, r, wtgt) + in + Hashtbl.add cached file tuple; + tuple + ) deps in - let _compiled, failed = + let opts = local_options, caches, cachet, cachec, cached in + let ok = if targets = [] then - make_aux root local_options [] [] deps + make_aux root opts true deps else - make_aux root local_options [] [] (purge_unwanted_roots targets deps) + make_aux root opts true (purge_unwanted_roots targets deps) in + print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout; HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; - failed = [] + time_stamp "L : 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