X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=2c2ba6ff2fcc9394d461849ec2d51cce85791dd1;hb=1652681b5eb49332f1c78e6c26d3ae5c7253d382;hp=b0c601f1f3120d89b116887d138c68c7fbc7a98d;hpb=2b53a3735b2a6130726e0a0451993cd679fd5935;p=helm.git diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index b0c601f1f..2c2ba6ff2 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -23,12 +23,12 @@ * http://helm.cs.unibo.it/ *) -let debug = ref true +let debug = ref 0 let time_stamp = let old = ref 0.0 in fun msg -> - if !debug then begin + 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 @@ -88,10 +88,24 @@ let load_root_file rootpath = lines ;; -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 +let find_root_for ~include_paths file = + 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 = @@ -111,17 +125,7 @@ let rec 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" -> - 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 = @@ -191,7 +195,9 @@ 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 @@ -202,15 +208,17 @@ 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 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 fst4 = function (x,_,_,_) -> x;; let modified_before_s_t (_,cs, ct, _, _) a b = - prerr_endline ("L s_t: a " ^ F.string_of_source_object a); - prerr_endline ("L s_t: b " ^ F.string_of_target_object 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 @@ -228,13 +236,17 @@ module Make = functor (F:Format) -> struct | Some a, Some b -> a <= b | _ -> false in - prerr_endline ("L s_t: " ^ string_of_bool r); r - let modified_before_t_t (_,_,ct, _, _) a b = -(* - prerr_endline ("L t_t: a " ^ F.string_of_target_object a); - prerr_endline ("L t_t: b " ^ F.string_of_target_object b); -*) let a = + if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r); + + r + + let modified_before_t_t (_,_,ct, _, _) a b = + + 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 @@ -259,124 +271,39 @@ module Make = functor (F:Format) -> struct with Not_found -> assert false in let r = match a, b with - | Some a, Some b -> -(* - prerr_endline ("tt: a " ^ string_of_float a); - prerr_endline ("tt: b " ^ string_of_float b); -*) - a <= b - | _ -> false + | Some a, Some b -> + + 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 - prerr_endline ("L t_t: " ^ string_of_bool r); r + + 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,_) = + let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = match r with | Some root -> not (F.is_readonly_buri_of opts f) | None -> assert false ;; -(* FG: Old sorting algorithm ************************************************) -(* - 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 modified_before_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 modified_before_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 = - time_stamp "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 - time_stamp "filter get_status: end"; - let todo = - let local, remote = - List.partition (fun (_,_,froot,_) -> froot = Some root) todo - in - let local, skipped = List.partition (is_not_ro opts) local in - List.iter - (fun x -> - HLog.warn("Read only baseuri for: "^F.string_of_source_object(fst4 x))) - skipped; - remote @ local - in - 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; - time_stamp "building"; - let r = F.build lo file in - time_stamp "done"; r - | Some froot -> make froot [file] - | None -> - HLog.error ("No root for: "^F.string_of_source_object file); - false - in - Hashtbl.add cc file rc; - ok && rc - ) - ok (List.rev todo) - in - make_aux root opts ok (List.rev deps) - end - else - ok -*) + (* FG: new sorting algorithm ************************************************) let rec make_aux root opts ok deps = @@ -384,17 +311,17 @@ module Make = functor (F:Format) -> struct and make_one root opts ok what = let lo, _, ct, cc, cd = opts in - let t, deps, froot, tgt = what 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 (_, _, _, _, 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 - prerr_endline ("L : processing " ^ str); + time_stamp ("L : processing " ^ str); try let r = Hashtbl.find cc t in - prerr_endline ("L : " ^ string_of_bool r ^ " " ^ str); + time_stamp ("L : " ^ string_of_bool r ^ " " ^ str); ok && r (* say "already built" *) with Not_found -> @@ -402,23 +329,23 @@ module Make = functor (F:Format) -> struct let res = if okd then if okt then true else - match froot with + let build path = match froot with | Some froot when froot = root -> - if is_not_ro opts what then begin - Hashtbl.remove ct tgt; - Hashtbl.add ct tgt None; - time_stamp ("L : BUILDING " ^ str); - let res = F.build lo t in - time_stamp ("L : DONE " ^ str); res - end else begin - HLog.warn("Read only baseuri for: "^ str); false - end - | Some froot -> make froot [t] - | None -> - HLog.error ("No root for: " ^ str); false + 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 + 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 - prerr_endline ("L : " ^ string_of_bool res ^ " " ^ str); + time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); Hashtbl.add cc t res; ok && res (****************************************************************************) @@ -430,6 +357,8 @@ module Make = functor (F:Format) -> struct 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 @@ -437,11 +366,21 @@ module Make = functor (F:Format) -> struct let deps = List.map (fun (file,d) -> - let r,tgt = F.root_and_target_of local_options file in + let r,path,wtgt,rotgt = 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); - Hashtbl.add cached file (file, d, r, tgt); - (file, d, r, tgt) + (* 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 @@ -450,9 +389,9 @@ module Make = functor (F:Format) -> struct if targets = [] then make_aux root opts true deps else - make_aux root opts true - (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; time_stamp "L : LEAVING";