]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.ml
...
[helm.git] / helm / software / components / library / librarian.ml
index f53de728c6a1ab554fed38f3bad8011c0d627f40..2c2ba6ff2fcc9394d461849ec2d51cce85791dd1 100644 (file)
@@ -1,4 +1,40 @@
-let debug = false;;
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * 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
 
@@ -40,7 +76,10 @@ let remove_trailing_slash s =
 let load_root_file rootpath =
   let data = HExtlib.input_file rootpath in
   let lines = Str.split (Str.regexp "\n") data in
-  let clean s = Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s) in
+  let clean s = 
+    Pcre.replace ~pat:"[ \t]+" ~templ:" "
+      (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s))
+  in
   List.map 
     (fun l -> 
       match Str.split (Str.regexp "=") l with
@@ -50,9 +89,23 @@ let load_root_file rootpath =
 ;;
 
 let 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 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 = 
@@ -72,11 +125,17 @@ let 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" -> 
-   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)
+;;
+
+let mk_baseuri root extra =
+  let chop name = 
+    assert(Filename.check_suffix name ".ma" ||
+      Filename.check_suffix name ".mma");
+    try Filename.chop_extension name
+    with Invalid_argument "Filename.chop_extension" -> name
+  in
+   remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra))
 ;;
 
 let baseuri_of_script ~include_paths file = 
@@ -92,16 +151,9 @@ let baseuri_of_script ~include_paths file =
     | _ -> raise (NoRootFor (file ^" "^path^" "^root))
   in
   let extra_buri = substract lpath lroot in
-  let chop name = 
-    assert(Filename.check_suffix name ".ma" ||
-      Filename.check_suffix name ".mma");
-    try Filename.chop_extension name
-    with Invalid_argument "Filename.chop_extension" -> name
-  in
   let extra = String.concat "/" extra_buri in
    root,
-   remove_trailing_slash (HExtlib.normalize_path 
-    (buri ^ "/" ^ chop extra)),
+   mk_baseuri buri extra,
    path,
    extra
 ;;
@@ -143,18 +195,30 @@ 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
   end
 
 module Make = functor (F:Format) -> struct
 
-  let say s = if debug then prerr_endline ("make: "^s);; 
+  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 younger_s_t (_,cs,ct) a b = 
+  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
@@ -162,23 +226,35 @@ module Make = functor (F:Format) -> struct
         | Some _ as x -> x
         | None ->
            match F.mtime_of_target_object b with
-           | Some t as x -> Hashtbl.add ct b x; x
+           | Some t as x -> 
+               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 -> a <= b
+       | _ -> false
+    in
+
+    if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r);
 
-  let younger_t_t (_,_,ct) a b = 
+    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.add ct a x; x
+          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
@@ -188,164 +264,155 @@ module Make = functor (F:Format) -> struct
         | Some _ as x -> x
         | None ->
            match F.mtime_of_target_object b with
-           | Some t as x -> Hashtbl.add ct b x; x
+           | Some t as x -> 
+              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 ->
 
-  let is_built opts t tgt = 
-    younger_s_t opts t tgt
-  ;;
+       if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a);
+       if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b);
 
-  let assoc4 l k = List.find (fun (k1,_,_,_) -> k1 = k) l;;
+          a <= b
+       | _ -> false
+    in
 
-  let fst4 = function (x,_,_,_) -> x;;
+    if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r);
 
-  let rec needs_build opts deps compiled (t,dependencies,root,tgt) =
-    say ("Checking if "^F.string_of_source_object t^ " needs to be built");
-    if List.mem t compiled then
-      (say "already compiled"; false)
-    else
-    if not (is_built opts t tgt) then
-      (say(F.string_of_source_object t^" is not built, thus needs to be built");
-      true)
-    else
-    try
-      let unsat =
-        List.find
-          (needs_build opts deps compiled) 
-          (List.map (assoc4 deps) dependencies)
-      in
-        say (F.string_of_source_object t^" depends on "^
-         F.string_of_source_object (fst4 unsat)^
-         " that needs to be built, thus needs to be built");
-        true
-    with Not_found ->
-      try 
-        let _,_,_,unsat = 
-          List.find 
-           (fun (_,_,_,tgt1) -> younger_t_t opts tgt tgt1) 
-           (List.map (assoc4 deps) dependencies)
-        in
-          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");
-          true
-      with Not_found -> false
-  ;;
-
-  let is_buildable opts compiled deps (t,dependencies,root,tgt as what) =
-    say ("Checking if "^F.string_of_source_object t^" is buildable");
-    let b = needs_build opts deps compiled what in
-    if not b then
-      (say (F.string_of_source_object t^
-       " does not need to be built, thus it not buildable");
-      false)
-    else
-    try  
-      let unsat,_,_,_ =
-        List.find (needs_build opts deps compiled) 
-          (List.map (assoc4 deps) dependencies)
-      in
-        say (F.string_of_source_object t^" depends on "^
-          F.string_of_source_object unsat^
-          " that needs build, thus is not buildable");
-        false
-    with Not_found -> 
-      say 
-        ("None of "^F.string_of_source_object t^
-        " dependencies needs to be built, thus it is buildable");
-      true
-  ;;
+    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 rec make_aux root (lo,_,ct as opts) compiled failed deps = 
-    let todo = List.filter (is_buildable opts compiled deps) deps in
-    let todo = List.filter (fun (f,_,_,_)->not (List.mem f failed)) todo in
-    if todo <> [] then
-      let compiled, failed = 
-        let todo =
-          let local, remote =
-            List.partition (fun (_,_,froot,_) -> froot = Some root) todo
+  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
-          remote @ local
-        in
-        List.fold_left 
-          (fun (c,f) (file,_,froot,tgt) ->
-            let rc = 
-              match froot with
-              | Some froot when froot = root -> 
-                  Hashtbl.remove ct tgt;
-                  Hashtbl.add ct tgt None;
-                  F.build lo file 
-              | Some froot -> make froot [file]
-              | None -> 
-                  HLog.error ("No root for: "^F.string_of_source_object file);
-                  false
-            in
-            if rc then (file::c,f)
-            else (c,file::f))
-          (compiled,failed) todo
-      in
-        make_aux root opts compiled failed deps
-    else
-      compiled, failed
+          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 = 
+(****************************************************************************)
+
+  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 caches,cachet = Hashtbl.create 73, Hashtbl.create 73 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,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); 
-          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
-    let opts = local_options, caches, cachet in
-    let _compiled, failed =
+    let opts = local_options, caches, cachet, cachec, cached in
+    let ok =
       if targets = [] then 
-        make_aux root opts [] [] deps
+        make_aux root opts true deps
       else
-        make_aux root opts [] [] (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;
-    failed = []
+    time_stamp "L : LEAVING";
+    ok
   ;;
 
 end
   
-let write_deps_file root deps =
-  let oc = open_out (root ^ "/depends") in
-  List.iter 
-    (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) 
-    deps;
-  close_out oc;
-  HLog.message ("Generated: " ^ root ^ "/depends")
-;;
+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