]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarian.ml
huge amount of work to make out Make crawl roots and
[helm.git] / components / library / librarian.ml
index 5918136764b6816c5b54dc5a2435d1093fdf02f9..f1649239460939d2915f226bc38b90312df3e82d 100644 (file)
@@ -1,6 +1,18 @@
 exception NoRootFor of string
 
+let absolutize path =
+ let path = 
+   if String.length path > 0 && path.[0] <> '/' then
+     Sys.getcwd () ^ "/" ^ path
+   else 
+     path
+ in
+   HExtlib.normalize_path path
+;;
+
+
 let find_root path =
+  let path = absolutize path in
   let paths = List.rev (Str.split (Str.regexp "/") path) in
   let rec build = function
     | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
@@ -8,7 +20,8 @@ let find_root path =
   in
   let paths = List.map HExtlib.normalize_path (build paths) in
   try HExtlib.find_in paths "root"
-  with Failure "find_in" -> raise (NoRootFor path)
+  with Failure "find_in" -> 
+    raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")"))
 ;;
   
 let ensure_trailing_slash s = 
@@ -22,7 +35,7 @@ let remove_trailing_slash s =
   if s.[len-1] = '/' then String.sub s 0 (len-1) else s
 ;;
 
-let parse_root rootpath =
+let load_root_file rootpath =
   let data = HExtlib.input_file rootpath in
   let lines = Str.split (Str.regexp "\n") data in
   List.map 
@@ -33,31 +46,35 @@ let parse_root rootpath =
     lines
 ;;
 
-
 let find_root_for ~include_paths file = 
  let include_paths = "" :: Sys.getcwd () :: include_paths in
- let path = HExtlib.find_in include_paths file in
- (* HLog.debug ("file "^file^" resolved as "^path); *)
- let rootpath, root, buri = 
-   try
-     let mburi = Helm_registry.get "matita.baseuri" in
-     match Str.split (Str.regexp " ") mburi with
-     | [root; buri] when HExtlib.is_prefix_of root path -> 
-         ":registry:", root, buri
-     | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
-   with Helm_registry.Key_not_found "matita.baseuri" -> 
-     let rootpath = find_root path in
-     let buri = List.assoc "baseuri" (parse_root rootpath) in
-     rootpath, Filename.dirname rootpath, buri
- in
- (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
- let uri = Http_getter_misc.strip_trailing_slash buri in
- 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
+ try 
+   let path = HExtlib.find_in include_paths file in
+   let path = absolutize path in
+   (* HLog.debug ("file "^file^" resolved as "^path); *)
+   let rootpath, root, buri = 
+     try
+       let mburi = Helm_registry.get "matita.baseuri" in
+       match Str.split (Str.regexp " ") mburi with
+       | [root; buri] when HExtlib.is_prefix_of root path -> 
+           ":registry:", root, buri
+       | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
+     with Helm_registry.Key_not_found "matita.baseuri" -> 
+       let rootpath = find_root path in
+       let buri = List.assoc "baseuri" (load_root_file rootpath) in
+       rootpath, Filename.dirname rootpath, buri
+   in
+   (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
+   let uri = Http_getter_misc.strip_trailing_slash buri in
+   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" as exn -> 
+   HLog.error ("Unable to find: "^file);
+   raise exn
 ;;
 
-let baseuri_of_script ?(include_paths=[]) file = 
+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
   let root = HExtlib.normalize_path root in
@@ -67,7 +84,7 @@ let baseuri_of_script ?(include_paths=[]) file =
     match l1, l2 with
     | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
     | l,[] -> l
-    | _ -> raise (NoRootFor file)
+    | _ -> raise (NoRootFor (file ^" "^path^" "^root))
   in
   let extra_buri = substract lpath lroot in
   let chop name = 
@@ -91,3 +108,187 @@ 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); exit 1
+        | 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 target_of: options -> source_object -> target_object
+    val string_of_source_object: source_object -> string
+    val string_of_target_object: target_object -> string
+    val build: options -> source_object -> bool
+    val root_of: options -> source_object -> string option
+    val mtime_of_source_object: source_object -> float option
+    val mtime_of_target_object: target_object -> float option
+  end
+
+module Make = functor (F:Format) -> struct
+
+  let prerr_endline _ = ();; 
+
+  let younger_s_t a b = 
+    match F.mtime_of_source_object a, F.mtime_of_target_object b with
+    | Some a, Some b -> a < b
+    | _ -> false (* XXX check if correct *)
+  ;;
+  let younger_t_t a b = 
+    match F.mtime_of_target_object a, F.mtime_of_target_object b with
+    | Some a, Some b -> a < b
+    | _ -> false (* XXX check if correct *)
+  ;;
+
+  let is_built opts t = younger_s_t t (F.target_of opts t);;
+
+  let rec needs_build opts deps compiled (t,dependencies) =
+    prerr_endline ("Checking if "^F.string_of_source_object t^" needs to be built");
+    if List.mem t compiled then
+      (prerr_endline "already compiled";
+      false)
+    else
+    if not (is_built opts t) then
+      (prerr_endline (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 (fun x -> x, List.assoc x deps) dependencies)
+      in
+        prerr_endline 
+         (F.string_of_source_object t^" depends on "^F.string_of_source_object (fst unsat)^
+         " that needs to be built, thus needs to be built");
+        true
+    with Not_found ->
+      try 
+        let unsat = 
+          List.find (younger_t_t (F.target_of opts t)) 
+           (List.map (F.target_of opts) dependencies)
+        in
+          prerr_endline 
+           (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) =
+    prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable");
+    let b = needs_build opts deps compiled (t,dependencies) in
+    if not b then
+      (prerr_endline (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 (fun x -> x, List.assoc x deps) dependencies)
+      in
+        prerr_endline 
+          (F.string_of_source_object t^" depends on "^
+          F.string_of_source_object (fst unsat)^
+          " that needs build, thus is not buildable");
+        false
+    with Not_found -> 
+      prerr_endline 
+        ("None of "^F.string_of_source_object t^
+        " dependencies needs to be built, thus it is buildable");
+      true
+  ;;
+
+  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 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
+    if todo <> [] then
+      let compiled, failed = 
+        let todo =
+          let local, remote =
+            List.partition
+              (fun (file,d) -> d<>[] || F.root_of local_options file = Some root)
+              todo
+          in
+          remote @ local
+        in
+        List.fold_left 
+          (fun (c,f) (file,_) ->
+            let froot = F.root_of local_options file in
+            let rc = 
+              match froot with
+              | Some froot when froot = root ->
+                  F.build local_options 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 local_options compiled failed deps
+    else
+      compiled, failed
+
+  and  make root targets = 
+    let deps = F.load_deps_file (root^"/depends") in
+    let local_options = load_root_file (root^"/root") in
+    HLog.debug ("Entering directory '"^root^"'");
+    let old_root = Sys.getcwd () in
+    Sys.chdir root;
+    let _compiled, failed =
+      if targets = [] then 
+        make_aux root local_options [] [] deps
+      else
+        make_aux root local_options [] [] (purge_unwanted_roots targets deps)
+    in
+    HLog.debug ("Leaving directory '"^root^"'");
+    Sys.chdir old_root;
+    failed = []
+  ;;
+
+end
+  
+let write_deps_file root deps =
+  let oc = open_out "depends" in
+  List.iter (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) deps;
+  close_out oc;
+  HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends")
+;;