]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.ml
Use seed to avoid further name clashes.
[helm.git] / helm / software / components / library / librarian.ml
index 124b1a1f5a57ece6cb0260e213986709543b6231..919edb36c4f9104eb88ec5be974016b12637533c 100644 (file)
@@ -40,7 +40,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
@@ -79,6 +82,16 @@ let find_root_for ~include_paths file =
    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 = 
   let root, buri, path = find_root_for ~include_paths file in
   let path = HExtlib.normalize_path path in
@@ -92,16 +105,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
 ;;
@@ -146,69 +152,99 @@ module type Format =
           options -> source_object -> string option * 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 prerr_endline 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 younger_s_t a fa b fb = 
-    let a = unopt_or_call a F.mtime_of_source_object fa in
-    let b = unopt_or_call b F.mtime_of_target_object fb in
-    match a,b with 
+  let younger_s_t (_,cs,ct) a 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
+    match a, b with 
     | Some a, Some b -> a < b
     | _ -> false
   ;;
 
-  let younger_t_t a fa b fb = 
-    let a = unopt_or_call a F.mtime_of_target_object fa in
-    let b = unopt_or_call b F.mtime_of_target_object fb in
+  let younger_t_t (_,_,ct) a 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 b;
+               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
     match a, b with
     | Some a, Some b -> a < b
     | _ -> false
   ;;
 
-  let is_built opts mt t mtgt tgt = 
-    younger_s_t mt t mtgt tgt
+  let is_built opts t tgt = 
+    younger_s_t opts t tgt
   ;;
 
-  let assoc6 l k = List.find (fun (k1,_,_,_,_,_) -> k1 = k) l;;
+  let assoc4 l k = List.find (fun (k1,_,_,_) -> k1 = k) l;;
 
-  let fst6 = function (x,_,_,_,_,_) -> x;;
+  let fst4 = function (x,_,_,_) -> x;;
 
-  let rec needs_build opts deps compiled (t,dependencies,root,tgt,mt,mtgt) =
-    prerr_endline ("Checking if "^F.string_of_source_object t^
-      " needs to be built");
+  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
-      (prerr_endline "already compiled";
-      false)
+      (say "already compiled"; false)
     else
-    if not (is_built opts mt t mtgt tgt) then
-      (prerr_endline (F.string_of_source_object t^
-       " is not built, thus needs to be built");
+    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 (assoc6 deps) dependencies)
+          (List.map (assoc4 deps) dependencies)
       in
-        prerr_endline 
-         (F.string_of_source_object t^" depends on "^
-         F.string_of_source_object (fst6 unsat)^
+        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,_,_ = 
+        let _,_,_,unsat = 
           List.find 
-           (fun (_,_,_,tgt1,_,mtgt1) -> younger_t_t mtgt tgt mtgt1 tgt1) 
-           (List.map (assoc6 deps) dependencies)
+           (fun (_,_,_,tgt1) -> younger_t_t opts tgt tgt1) 
+           (List.map (assoc4 deps) dependencies)
         in
-          prerr_endline 
+          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");
@@ -216,26 +252,25 @@ module Make = functor (F:Format) -> struct
       with Not_found -> false
   ;;
 
-  let is_buildable opts compiled deps (t,dependencies,root,tgt,_,_ as what) =
-    prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable");
+  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
-      (prerr_endline (F.string_of_source_object t^
+      (say (F.string_of_source_object t^
        " does not need to be built, thus it not buildable");
       false)
     else
     try  
-      let unsat,_,_,_,_,_ =
+      let unsat,_,_,_ =
         List.find (needs_build opts deps compiled) 
-          (List.map (assoc6 deps) dependencies)
+          (List.map (assoc4 deps) dependencies)
       in
-        prerr_endline 
-          (F.string_of_source_object t^" depends on "^
+        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 -> 
-      prerr_endline 
+      say 
         ("None of "^F.string_of_source_object t^
         " dependencies needs to be built, thus it is buildable");
       true
@@ -244,37 +279,48 @@ module Make = functor (F:Format) -> struct
   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,_) =
+    match r with
+    | Some root -> not (F.is_readonly_buri_of opts f)
+    | None -> assert false
+  ;;
 
-  let rec make_aux root local_options compiled failed deps = 
-    let todo = List.filter (is_buildable local_options compiled deps) deps in
-    let todo = List.filter (fun (f,_,_,_,_,_)->not (List.mem f failed)) todo in
+  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
+    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
       let compiled, failed = 
-        let todo =
-          let local, remote =
-            List.partition (fun (_,_,froot,_,_,_) -> froot = Some root) todo
-          in
-          remote @ local
-        in
         List.fold_left 
-          (fun (c,f) (file,_,froot,_,_,_) ->
+          (fun (c,f) (file,_,froot,tgt) ->
             let rc = 
               match froot with
-              | Some froot when froot = root ->
-                  F.build local_options file 
-              | Some froot ->
-                  make froot [file]
+              | 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
@@ -283,7 +329,7 @@ module Make = functor (F:Format) -> struct
             else (c,file::f))
           (compiled,failed) todo
       in
-        make_aux root local_options compiled failed deps
+        make_aux root opts compiled failed deps
     else
       compiled, failed
 
@@ -293,20 +339,24 @@ module Make = functor (F:Format) -> struct
     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
+    (* deps are enriched with these informations to sped up things later *)
     let deps = 
       List.map 
         (fun (file,d) -> 
-                HLog.debug (F.string_of_source_object file);
           let r,tgt = F.root_and_target_of local_options file in
-          file, d, r, tgt, F.mtime_of_source_object file, 
-          F.mtime_of_target_object tgt) 
+          Hashtbl.add caches file (F.mtime_of_source_object file);
+          Hashtbl.add cachet tgt (F.mtime_of_target_object tgt); 
+          file, d, r, tgt)
         deps
     in
+    let opts = local_options, caches, cachet in
     let _compiled, failed =
       if targets = [] then 
-        make_aux root local_options [] [] deps
+        make_aux root opts [] [] deps
       else
-        make_aux root local_options [] [] (purge_unwanted_roots targets deps)
+        make_aux root opts [] [] 
+          (purge_unwanted_roots targets deps)
     in
     HLog.debug ("Leaving directory '"^root^"'");
     Sys.chdir old_root;
@@ -315,12 +365,19 @@ module Make = functor (F:Format) -> struct
 
 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