From 3c8a3783837bf7773437b12a089b8edf93879b5d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 6 Jan 2008 20:46:39 +0000 Subject: [PATCH] huge amount of work to make out Make crawl roots and compile recursively what is needed --- components/cic_disambiguation/.depend | 4 +- components/cic_disambiguation/.depend.opt | 4 +- components/grafite_parser/.depend | 4 +- components/grafite_parser/.depend.opt | 4 +- components/library/.depend.opt | 2 + components/library/librarian.ml | 249 +++++++++++++++++++--- components/library/librarian.mli | 31 ++- matita/.depend | 8 +- matita/.depend.opt | 66 +++--- matita/Makefile | 6 +- matita/make.ml | 143 ------------- matita/make.mli | 22 -- matita/matitaScript.ml | 9 +- matita/matitaScript.mli | 2 +- matita/matitac.ml | 19 +- matita/matitacLib.ml | 42 +++- matita/matitacLib.mli | 2 +- matita/matitadep.ml | 49 +++-- 18 files changed, 376 insertions(+), 290 deletions(-) delete mode 100644 matita/make.ml delete mode 100644 matita/make.mli diff --git a/components/cic_disambiguation/.depend b/components/cic_disambiguation/.depend index ca4124461..2ca28ce61 100644 --- a/components/cic_disambiguation/.depend +++ b/components/cic_disambiguation/.depend @@ -8,5 +8,5 @@ disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \ disambiguate.cmi disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ disambiguate.cmi -number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx +number_notation.cmo: disambiguateChoices.cmi +number_notation.cmx: disambiguateChoices.cmx diff --git a/components/cic_disambiguation/.depend.opt b/components/cic_disambiguation/.depend.opt index ca4124461..2ca28ce61 100644 --- a/components/cic_disambiguation/.depend.opt +++ b/components/cic_disambiguation/.depend.opt @@ -8,5 +8,5 @@ disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \ disambiguate.cmi disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ disambiguate.cmi -number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx +number_notation.cmo: disambiguateChoices.cmi +number_notation.cmx: disambiguateChoices.cmx diff --git a/components/grafite_parser/.depend b/components/grafite_parser/.depend index 2dc8a7cab..f097cc8d3 100644 --- a/components/grafite_parser/.depend +++ b/components/grafite_parser/.depend @@ -1,8 +1,8 @@ grafiteWalker.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi -grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi -grafiteParser.cmx: dependenciesParser.cmx grafiteParser.cmi +grafiteParser.cmo: grafiteParser.cmi +grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi grafiteDisambiguator.cmo: grafiteDisambiguator.cmi diff --git a/components/grafite_parser/.depend.opt b/components/grafite_parser/.depend.opt index 2dc8a7cab..f097cc8d3 100644 --- a/components/grafite_parser/.depend.opt +++ b/components/grafite_parser/.depend.opt @@ -1,8 +1,8 @@ grafiteWalker.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi -grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi -grafiteParser.cmx: dependenciesParser.cmx grafiteParser.cmi +grafiteParser.cmo: grafiteParser.cmi +grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi grafiteDisambiguator.cmo: grafiteDisambiguator.cmi diff --git a/components/library/.depend.opt b/components/library/.depend.opt index 190aaf9b7..d8ff04797 100644 --- a/components/library/.depend.opt +++ b/components/library/.depend.opt @@ -1,5 +1,7 @@ cicCoercion.cmi: coercDb.cmi librarySync.cmi: refinementTool.cmx +librarian.cmo: librarian.cmi +librarian.cmx: librarian.cmi cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi cicRecord.cmo: cicRecord.cmi 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") +;; + diff --git a/components/library/librarian.mli b/components/library/librarian.mli index 90b7ef168..839d8daa1 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -2,7 +2,7 @@ exception NoRootFor of string val find_root: string -> string -val parse_root: string -> (string*string) list +(* val parse_root: string -> (string*string) list *) (* baseuri_of_script ?(inc:REG[matita.includes]) fname * -> @@ -10,7 +10,34 @@ val parse_root: string -> (string*string) list * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, * /home/pippo/devel/a.ma *) val baseuri_of_script: - ?include_paths:string list -> string -> string * string * string * string + include_paths:string list -> string -> string * string * string * string (* finds all the roots files in the specified dir *) val find_roots_in_dir: string -> string list + +(* make *) +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) -> + sig + (* make [root dir] [targets], targets = [] means make all *) + val make : string -> F.source_object list -> bool + end + +val load_deps_file: string -> (string * string list) list +val write_deps_file: string -> (string * string list) list -> unit diff --git a/matita/.depend b/matita/.depend index 1530bae72..d6d6aefc4 100644 --- a/matita/.depend +++ b/matita/.depend @@ -4,8 +4,6 @@ dump_moo.cmo: buildTimeConf.cmo dump_moo.cmx: buildTimeConf.cmx lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi -make.cmo: make.cmi -make.cmx: make.cmi matitaAutoGui.cmo: matitaGeneratedGui.cmo applyTransformation.cmi \ matitaAutoGui.cmi matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ @@ -17,9 +15,9 @@ matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \ matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ - matitaWiki.cmo matitaMisc.cmi matitaInit.cmi matitaEngine.cmi make.cmi + matitaWiki.cmo matitaMisc.cmi matitaInit.cmi matitaEngine.cmi matitac.cmx: matitaprover.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ - matitaWiki.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx make.cmx + matitaWiki.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -70,8 +68,6 @@ matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmo applyTransformation.cmi matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx applyTransformation.cmx -rottener.cmo: matitaInit.cmi buildTimeConf.cmo -rottener.cmx: matitaInit.cmx buildTimeConf.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo diff --git a/matita/.depend.opt b/matita/.depend.opt index 933d2bb51..db22851e4 100644 --- a/matita/.depend.opt +++ b/matita/.depend.opt @@ -2,24 +2,22 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi dump_moo.cmo: buildTimeConf.cmx dump_moo.cmx: buildTimeConf.cmx -gragrep.cmo: matitaInit.cmi buildTimeConf.cmx gragrep.cmi -gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi -matitaAutoGui.cmo: matitaGeneratedGui.cmx matitaAutoGui.cmi -matitaAutoGui.cmx: matitaGeneratedGui.cmx matitaAutoGui.cmi +matitaAutoGui.cmo: matitaGeneratedGui.cmx applyTransformation.cmi \ + matitaAutoGui.cmi +matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ + matitaAutoGui.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmx \ +matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmx \ applyTransformation.cmi matitacLib.cmi -matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ +matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitacLib.cmi -matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi matitaWiki.cmx matitaInit.cmi matitaEngine.cmi gragrep.cmi -matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx +matitac.cmo: matitaprover.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ + matitaWiki.cmx matitaMisc.cmi matitaInit.cmi matitaEngine.cmi +matitac.cmx: matitaprover.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ + matitaWiki.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -30,30 +28,22 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.cmi \ - matitaScript.cmi matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ +matitaGui.cmo: matitaprover.cmi matitaTypes.cmi matitaScript.cmi \ + matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ matitaGeneratedGui.cmx matitaExcPp.cmi matitaAutoGui.cmi \ buildTimeConf.cmx matitaGui.cmi -matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \ - matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ +matitaGui.cmx: matitaprover.cmx matitaTypes.cmx matitaScript.cmx \ + matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx matitaAutoGui.cmx \ buildTimeConf.cmx matitaGui.cmi -matitaInit.cmo: matitamakeLib.cmi matitaExcPp.cmi buildTimeConf.cmx \ - matitaInit.cmi -matitaInit.cmx: matitamakeLib.cmx matitaExcPp.cmx buildTimeConf.cmx \ - matitaInit.cmi -matitamakeLib.cmo: buildTimeConf.cmx matitamakeLib.cmi -matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitamake.cmi -matitaMathView.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - lablGraphviz.cmi buildTimeConf.cmx applyTransformation.cmi \ - matitaMathView.cmi -matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - lablGraphviz.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaMathView.cmi +matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi +matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi +matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ + buildTimeConf.cmx applyTransformation.cmi matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmx matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ @@ -66,12 +56,12 @@ matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmx matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitaprover.cmi -matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmx \ - applyTransformation.cmi matitaScript.cmi -matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaScript.cmi +matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi buildTimeConf.cmx applyTransformation.cmi \ + matitaScript.cmi +matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \ + matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ diff --git a/matita/Makefile b/matita/Makefile index 6d1135a23..b3fbd5906 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -28,7 +28,6 @@ ifeq ($(NODB),true) endif MLI = \ - make.mli \ lablGraphviz.mli \ matitaTypes.mli \ matitaMisc.mli \ @@ -45,7 +44,6 @@ MLI = \ matitaGui.mli \ $(NULL) CMLI = \ - make.mli \ matitaTypes.mli \ matitaMisc.mli \ matitaExcPp.mli \ @@ -111,9 +109,9 @@ links: linkonly: $(H)echo " OCAMLC matita.ml" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) matita.ml + $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml $(H)echo " OCAMLC matitac.ml" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) matitac.ml + $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml .PHONY: linkonly matita: matita.ml $(LIB_DEPS) $(CMOS) $(H)echo " OCAMLC $<" diff --git a/matita/make.ml b/matita/make.ml deleted file mode 100644 index b1136642a..000000000 --- a/matita/make.ml +++ /dev/null @@ -1,143 +0,0 @@ - -module type Format = sig - - type source_object - type target_object - - val target_of : source_object -> target_object - val string_of_source_object : source_object -> string - val string_of_target_object : target_object -> string - - val build : source_object -> bool - - 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 t = younger_s_t t (F.target_of t);; - - let rec needs_build 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 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 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 t)) (List.map F.target_of 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 compiled deps (t,dependencies) = - prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable"); - let b = needs_build 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 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 make compiled failed deps = - let todo = List.filter (is_buildable compiled deps) deps in - let todo = List.filter (fun (f,_) -> not (List.mem f failed)) todo in - if todo <> [] then - let compiled, failed = - List.fold_left - (fun (c,f) (file,_) -> - if F.build file then (file::c,f) - else (c,file::f)) - (compiled,failed) todo - in - make compiled failed deps - ;; - - 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 make deps targets = - if targets = [] then - make [] [] deps - else - make [] [] (purge_unwanted_roots targets deps) - ;; - -end - -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"; exit 1 - | he::tl -> deps := (he,tl) :: !deps - end - done; !deps - with End_of_file -> !deps -;; diff --git a/matita/make.mli b/matita/make.mli deleted file mode 100644 index 883586c46..000000000 --- a/matita/make.mli +++ /dev/null @@ -1,22 +0,0 @@ - -module type Format = - sig - type source_object - type target_object - val target_of : source_object -> target_object - val string_of_source_object : source_object -> string - val string_of_target_object : target_object -> string - val build : source_object -> bool - val mtime_of_source_object : source_object -> float option - val mtime_of_target_object : target_object -> float option - end - -module Make : - functor (F : Format) -> - sig - (* make [deps] [targets], targets = [] means make all *) - val make : (F.source_object * F.source_object list) list -> - F.source_object list -> unit - end - -val load_deps_file: string -> (string * string list) list diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index d5cad512a..9dc930f18 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -720,11 +720,15 @@ object (self) method has_name = filename_ <> None - method buri_of_current_file = + method buri_of_current_file = match filename_ with | None -> default_buri | Some f -> - try let _root, buri, _fname, _tgt = Librarian.baseuri_of_script f in buri + try + let _root, buri, _fname, _tgt = + Librarian.baseuri_of_script ~include_paths f + in + buri with Librarian.NoRootFor _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f @@ -1105,7 +1109,6 @@ prerr_endline ("## " ^ string_of_int parsed_text_length); HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; HLog.debug ("Current file name: " ^ self#filename); - HLog.debug ("Current buri: " ^ self#buri_of_current_file); end let _script = ref None diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli index 89986ead7..e8b80d25b 100644 --- a/matita/matitaScript.mli +++ b/matita/matitaScript.mli @@ -55,7 +55,7 @@ object method has_name: bool (* alwais return a name, use has_name to check if it is the default one *) method filename: string - method buri_of_current_file: string + method buri_of_current_file: string method assignFileName : string option -> unit (* to the current active file *) method loadFromFile : string -> unit method loadFromString : string -> unit diff --git a/matita/matitac.ml b/matita/matitac.ml index 199b04157..f52db24a6 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -87,31 +87,34 @@ let dump f = (* compiler ala pascal/java using make *) let main_compiler () = MatitaInit.initialize_all (); + if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); (* targets and deps *) let targets = Helm_registry.get_list Helm_registry.string "matita.args" in - let deps, target = + let target, root = match targets with | [] -> (match Librarian.find_roots_in_dir (Sys.getcwd ()) with - | [x] -> - Make.load_deps_file (Filename.dirname x ^ "/depends"), [] + | [x] -> [], x | [] -> HLog.error "No targets and no root found"; exit 1 | roots -> HLog.error ("Too many roots found, move into one and retry: "^ String.concat ", " roots);exit 1); | [hd] -> - let root, buri, file, target = Librarian.baseuri_of_script hd in - HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'"); - Make.load_deps_file (root ^ "/depends"), [target] + let root, buri, file, target = + Librarian.baseuri_of_script ~include_paths:[] hd + in + [target], root | _ -> HLog.error "Only one target (or none) can be specified.";exit 1 in (* must be called after init since args are set by cmdline parsing *) let system_mode = Helm_registry.get_bool "matita.system" in if system_mode then HLog.message "Compiling in system space"; - if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); (* here we go *) - MatitacLib.Make.make deps target + if MatitacLib.Make.make root target then + HLog.message "Compilation successful" + else + HLog.message "Compilation failed" ;; let main () = diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 5886c2467..3c3d421a5 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -95,14 +95,24 @@ let cut prefix s = String.sub s lenp (lens-lenp) ;; -let rec compile fname = - (* initialization, MOVE OUTSIDE *) - let matita_debug = Helm_registry.get_bool "matita.debug" in - let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in +let get_include_paths options = let include_paths = + try List.assoc "include_paths" options with Not_found -> "" + in + let include_paths = Str.split (Str.regexp " ") include_paths in + let include_paths = + include_paths @ Helm_registry.get_list Helm_registry.string "matita.includes" in + include_paths +;; + +let rec compile options fname = + (* initialization, MOVE OUTSIDE *) + let matita_debug = Helm_registry.get_bool "matita.debug" in + let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in (* sanity checks *) + let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true @@ -204,7 +214,7 @@ let rec compile fname = ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") in !out str; - compile fname + compile options fname | _ -> let x, y = HExtlib.loc_of_floc floc in HLog.error (sprintf "A macro has been found at %d-%d" x y); @@ -229,8 +239,17 @@ module F = let string_of_source_object s = s;; let string_of_target_object s = s;; - let target_of mafile = - let _,baseuri,_,_ = Librarian.baseuri_of_script mafile in + let root_of opts s = + try + let include_paths = get_include_paths opts in + let root,_,_,_ = Librarian.baseuri_of_script ~include_paths s in + Some root + with Librarian.NoRootFor x -> None + ;; + + let target_of opts mafile = + let include_paths = get_include_paths opts in + let _,baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mafile in LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true ;; @@ -238,7 +257,9 @@ module F = let mtime_of_source_object s = try Some (Unix.stat s).Unix.st_mtime with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> - raise (Failure ("Unable to stat a source file: " ^ s)) + None +(* max_float *) +(* raise (Failure ("Unable to stat a source file: " ^ s)) *) ;; let mtime_of_target_object s = @@ -247,7 +268,10 @@ module F = ;; let build = compile;; + + let load_deps_file = Librarian.load_deps_file;; + end -module Make = Make.Make(F) +module Make = Librarian.Make(F) diff --git a/matita/matitacLib.mli b/matita/matitacLib.mli index b126df3a1..03ea56beb 100644 --- a/matita/matitacLib.mli +++ b/matita/matitacLib.mli @@ -27,6 +27,6 @@ val set_callback: (string -> unit) -> unit module Make : sig - val make: (string * string list) list -> string list -> unit + val make: string -> string list -> bool end diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 6a2dccb91..42034c1a8 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -66,9 +66,7 @@ let main () = " Save dependency graph in dot format to the given file";]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment (); - let args = Helm_registry.get_list Helm_registry.string "matita.args" in let args = - if args = [] then let roots = Librarian.find_roots_in_dir (Sys.getcwd ()) in match roots with | [] -> @@ -81,8 +79,6 @@ let main () = prerr_endline ("Too many roots: " ^ String.concat ", " roots); prerr_endline ("Enter one of these directories and retry"); exit 1 - else - args in let ma_files = args in (* here we go *) @@ -133,24 +129,35 @@ let main () = close_out oc end; (* generate regular depend output *) - let oc = open_out "depends" in - List.iter - (fun ma_file -> + let fix_name f = + let f = + if Pcre.pmatch ~pat:"^\\./" f then + String.sub f 2 (String.length f - 2) + else + f + in + HExtlib.normalize_path f + in + let deps = + List.fold_left + (fun acc ma_file -> let deps = Hashtbl.find_all include_deps ma_file in let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in - let deps = ma_file :: deps in - let deps = - List.map (fun f -> - let f = - if Pcre.pmatch ~pat:"^\\./" f then - String.sub f 2 (String.length f - 2) - else - f - in HExtlib.normalize_path f) deps - in - output_string oc (String.concat " " deps ^ "\n")) - ma_files; - close_out oc; - HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends") + let deps = List.map fix_name deps in + (fix_name ma_file, deps) :: acc) + [] ma_files + in + let extern = + List.fold_left + (fun acc (_,d) -> + List.fold_left + (fun a x -> + if List.exists (fun (t,_) -> x=t) deps then a + else x::a) + acc d) + [] deps + in + Librarian.write_deps_file (Sys.getcwd()) (deps@List.map (fun x -> x,[]) extern) +;; -- 2.39.2