]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.ml
we commented some of the debug pps rather than removing them :)
[helm.git] / helm / software / components / library / librarian.ml
index 8b7bdb09fa05b304f1370be67d330d851d60cce3..6cedc0101a4aee756897d198b2d605128139fac9 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-let debug = false;;
+let debug = ref 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
+let time_stamp =
+   let old = ref 0.0 in
+   fun msg -> 
+      if !debug 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
 
@@ -84,7 +88,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
@@ -108,10 +112,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 =
@@ -192,13 +202,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 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 younger_s_t (_,cs, ct, _, _) a b = 
+  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);
+*)
     let a = try Hashtbl.find cs a with Not_found -> assert false in
     let b = 
       try
@@ -212,20 +226,28 @@ module Make = functor (F:Format) -> struct
            | x -> x
       with Not_found -> assert false
     in
-    match a, b with 
-    | Some a, Some b -> a < b
-    | _ -> false
-  ;;
+    let r = match a, b with 
+       | Some a, Some b -> a <= b
+       | _ -> false
+    in
+(*    
+    time_stamp ("L s_t: " ^ string_of_bool r);
+*)    
+    r
 
-  let younger_t_t (_,_,ct, _, _) a b = 
+  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);
+*) 
     let a = 
       try
         match Hashtbl.find ct a with
         | Some _ as x -> x
         | None ->
-           match F.mtime_of_target_object a with
+          match F.mtime_of_target_object a with
            | Some t as x -> 
-               Hashtbl.remove ct b;
+              Hashtbl.remove ct a;
                Hashtbl.add ct a x; x
            | x -> x
       with Not_found -> assert false
@@ -237,15 +259,24 @@ module Make = functor (F:Format) -> struct
         | None ->
            match F.mtime_of_target_object b with
            | Some t as x -> 
-               Hashtbl.remove ct b;
+              Hashtbl.remove ct b;
                Hashtbl.add ct b x; x
            | x -> x
       with Not_found -> assert false
     in
-    match a, b with
-    | Some a, Some b -> a < b
-    | _ -> false
-  ;;
+    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);
+*)       
+          a <= b
+       | _ -> false
+    in
+(*    
+    time_stamp ("L t_t: " ^ string_of_bool r);
+*)    
+    r
 
   let rec purge_unwanted_roots wanted deps =
     let roots, rest = 
@@ -266,7 +297,8 @@ module Make = functor (F:Format) -> struct
     | 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
@@ -282,7 +314,7 @@ module Make = functor (F:Format) -> struct
              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  
+                   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
@@ -291,7 +323,7 @@ module Make = functor (F:Format) -> struct
                 | _                     -> st
              end
        in
-        let st = if younger_s_t opts t tgt then Done true else Ready true 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" *)
@@ -310,13 +342,13 @@ module Make = functor (F:Format) -> struct
      aux [] [] l
 
   let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps = 
-    timestamp "filter get_status: begin";
+    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
-    timestamp "filter get_status: end";
+    time_stamp "filter get_status: end";
     let todo =
       let local, remote =
         List.partition (fun (_,_,froot,_) -> froot = Some root) todo
@@ -334,11 +366,11 @@ module Make = functor (F:Format) -> struct
             let rc = 
               match froot with
               | Some froot when froot = root -> 
-                  Hashtbl.remove ct tgt;
+                 Hashtbl.remove ct tgt;
                   Hashtbl.add ct tgt None;
-                  timestamp "building";
+                  time_stamp "building";
                  let r = F.build lo file in
-                 timestamp "done"; r
+                 time_stamp "done"; r
               | Some froot -> make froot [file]
               | None -> 
                   HLog.error ("No root for: "^F.string_of_source_object file);
@@ -353,9 +385,55 @@ module Make = functor (F:Format) -> struct
     end
     else
       ok
+*)
+(* FG: new sorting algorithm ************************************************)
+
+  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, 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
+          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
+          else false
+       in
+       time_stamp ("L : " ^ string_of_bool res ^ " " ^ str);
+       Hashtbl.add cc t res; ok && res
+
+(****************************************************************************)
 
-  and  make root targets = 
-    timestamp "entering";
+  and make root targets = 
+    time_stamp "L : ENTERING";
     HLog.debug ("Entering directory '"^root^"'");
     let old_root = Sys.getcwd () in
     Sys.chdir root;
@@ -386,7 +464,7 @@ module Make = functor (F:Format) -> struct
     in
     HLog.debug ("Leaving directory '"^root^"'");
     Sys.chdir old_root;
-    timestamp "leaving";
+    time_stamp "L : LEAVING";
     ok
   ;;