X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2Flibrarian.ml;h=f1649239460939d2915f226bc38b90312df3e82d;hb=3c8a3783837bf7773437b12a089b8edf93879b5d;hp=5918136764b6816c5b54dc5a2435d1093fdf02f9;hpb=4a62bde42e3655a7829b9281d9b9057dc32c0471;p=helm.git diff --git a/components/library/librarian.ml b/components/library/librarian.ml index 591813676..f16492394 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -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") +;; +