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 | [] -> ["/"] in let paths = List.map HExtlib.normalize_path (build paths) in try HExtlib.find_in paths "root" with Failure "find_in" -> raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")")) ;; let ensure_trailing_slash s = if s = "" then "/" else if s.[String.length s-1] <> '/' then s^"/" else s ;; let remove_trailing_slash s = if s = "" then "" else let len = String.length s in if s.[len-1] = '/' then String.sub s 0 (len-1) else s ;; let load_root_file rootpath = let data = HExtlib.input_file rootpath in let lines = Str.split (Str.regexp "\n") data in List.map (fun l -> match Str.split (Str.regexp "=") l with | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) lines ;; 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 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" -> HLog.error ("Unable to find: "^file^"\nPaths explored:\n"); List.iter (fun x -> HLog.error (" - "^x^"\n")) include_paths; raise (NoRootFor 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 let lpath = Str.split (Str.regexp "/") path in let lroot = Str.split (Str.regexp "/") root in let rec substract l1 l2 = match l1, l2 with | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2 | l,[] -> l | _ -> raise (NoRootFor (file ^" "^path^" "^root)) in let extra_buri = substract lpath lroot in let chop name = assert(Filename.check_suffix name ".ma"); 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)), path, extra ;; let find_roots_in_dir dir = HExtlib.find ~test:(fun f -> Filename.basename f = "root" && try (Unix.stat f).Unix.st_kind = Unix.S_REG with Unix.Unix_error _ -> false) 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") ;;