]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.ml
BTop is a category.
[helm.git] / helm / software / components / library / librarian.ml
index f56ba5840cda99a19b44ea95d38e9a57b7b3a5a1..32b6de48bfd6a599b905ee30820f6f5457839a90 100644 (file)
@@ -204,7 +204,7 @@ module Make = functor (F:Format) -> struct
 
   let fst4 = function (x,_,_,_) -> x;;
 
-  let younger_s_t (_,cs, ct, _, _) a b = 
+  let modified_before_s_t (_,cs, ct, _, _) a b = 
     let a = try Hashtbl.find cs a with Not_found -> assert false in
     let b = 
       try
@@ -223,7 +223,7 @@ module Make = functor (F:Format) -> struct
     | _ -> false
   ;;
 
-  let younger_t_t (_,_,ct, _, _) a b = 
+  let modified_before_t_t (_,_,ct, _, _) a b = 
     let a = 
       try
         match Hashtbl.find ct a with
@@ -231,7 +231,7 @@ module Make = functor (F:Format) -> struct
         | None ->
            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
@@ -272,7 +272,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
@@ -288,7 +289,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
@@ -297,7 +298,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" *)
@@ -340,7 +341,7 @@ 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";
                  let r = F.build lo file in
@@ -359,8 +360,48 @@ 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 map (okd, okt) d =
+       let (_, _, _, tgtd) as whatd = (Hashtbl.find cd d) in
+       make_one root opts okd whatd, okt && modified_before_t_t opts tgtd tgt
+    in
+    try ok && Hashtbl.find cc t
+(* 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 str = F.string_of_source_object t in
+          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;
+                   timestamp "building";
+                  let res = F.build lo t in
+                  timestamp "done"; 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
+       Hashtbl.add cc t res; ok && res
+
+(****************************************************************************)
 
-  and  make root targets = 
+  and make root targets = 
     timestamp "entering";
     HLog.debug ("Entering directory '"^root^"'");
     let old_root = Sys.getcwd () in