* http://helm.cs.unibo.it/
*)
-let debug = ref false
+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
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 =
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 =
val build: options -> source_object -> bool
val root_and_target_of:
options -> source_object ->
- (* root, writeable target, read only target *)
- string option * target_object * target_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
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 =
-(*
- time_stamp ("L s_t: a " ^ F.string_of_source_object a);
- time_stamp ("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
| Some a, Some b -> a <= b
| _ -> false
in
-(*
- time_stamp ("L s_t: " ^ string_of_bool r);
-*)
+
+ if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r);
+
r
let modified_before_t_t (_,_,ct, _, _) a b =
-(*
- time_stamp ("L t_t: a " ^ F.string_of_target_object a);
- time_stamp ("L t_t: b " ^ F.string_of_target_object 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
in
let r = match a, b with
| Some a, Some b ->
-(*
- time_stamp ("tt: a " ^ string_of_float a);
- time_stamp ("tt: b " ^ string_of_float 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
-(*
- time_stamp ("L t_t: " ^ string_of_bool 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 =
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
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.error ("Read only baseuri for: "^ str^
- ", I won't compile it even if it is out of date");
- 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
time_stamp ("L : " ^ string_of_bool res ^ " " ^ str);
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
let deps =
List.map
(fun (file,d) ->
- let r,wtgt,rotgt = 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);
(* if a read only target exists, we use that one, otherwise
we use the writeable one that may be compiled *)
- let _,_,_, tgt as tuple =
+ let _,_,_,_, tgt as tuple =
match F.mtime_of_target_object rotgt with
| Some _ as mtime ->
Hashtbl.add cachet rotgt mtime;
- (file, d, r, rotgt)
+ (file, path, d, r, rotgt)
| None ->
Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt);
- (file, d, r, wtgt)
+ (file, path, d, r, wtgt)
in
Hashtbl.add cached file tuple;
tuple
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";
projects / helm.git / commitdiff