]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/library/librarian.ml
Huge change!!!
[helm.git] / matita / components / library / librarian.ml
index 2c2ba6ff2fcc9394d461849ec2d51cce85791dd1..7d159af2467a26cddfac6ef9e4863a42961db0d4 100644 (file)
  * 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
 
 let absolutize path =
@@ -166,253 +153,7 @@ let find_roots_in_dir dir =
     dir
 ;;
 
-(* make *)
-let load_deps_file f = 
-  let deps = ref [] in
-  let ic = open_in f in
-  try
-    while true do
-      begin
-        let l = input_line ic in
-        match Str.split (Str.regexp " ") l with
-        | [] -> 
-            HLog.error ("Malformed deps file: " ^ f); 
-            raise (Failure ("Malformed deps file: " ^ f)) 
-        | he::tl -> deps := (he,tl) :: !deps
-      end
-    done; !deps
-    with End_of_file -> !deps
-;;
-
-type options = (string * string) list
-
-module type Format =
-  sig
-    type source_object
-    type target_object
-    val load_deps_file: string -> (source_object * source_object list) list
-    val string_of_source_object: source_object -> string
-    val string_of_target_object: target_object -> string
-    val build: options -> source_object -> bool
-    val root_and_target_of: 
-          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
-
-  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 fst4 = function (x,_,_,_) -> x;;
-
-  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
-
-    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
-        | 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 ->
-
-       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))
-         deps
-    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 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
-          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 = 
-    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) -> 
-          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 opts = local_options, caches, cachet, cachec, cached in
-    let ok =
-      if targets = [] then 
-        make_aux root opts true deps
-      else
-        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";
-    ok
-  ;;
-
-end
-  
-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
+let is_uri str = Pcre.pmatch ~rex:uri_scheme_rex str