huge amount of work to make out Make crawl roots and

compile recursively what is needed

diff --git a/components/cic_disambiguation/.depend b/components/cic_disambiguation/.depend
index ca41244617a50c99cb10483c7cbd24ff162aaba1..2ca28ce61aad63756e8713cb8f7cba790b6b6a2e 100644 (file)
--- 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 ca41244617a50c99cb10483c7cbd24ff162aaba1..2ca28ce61aad63756e8713cb8f7cba790b6b6a2e 100644 (file)
--- 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 2dc8a7cab3c91b0c51d7f42b68ff98ab5ff40a2b..f097cc8d3af5c1df6e3c79bc97c0439558f01bb7 100644 (file)
--- 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 2dc8a7cab3c91b0c51d7f42b68ff98ab5ff40a2b..f097cc8d3af5c1df6e3c79bc97c0439558f01bb7 100644 (file)
--- 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 190aaf9b7ed952df67f019f3f11da1f30b47656e..d8ff04797645c5804394afb7282e346a3075bbc5 100644 (file)
--- 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 5918136764b6816c5b54dc5a2435d1093fdf02f9..f1649239460939d2915f226bc38b90312df3e82d 100644 (file)
--- 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 90b7ef168e64a265a1f24400a4846fa5ea2c0568..839d8daa1e80381b3aba4faed09bee8a520cf471 100644 (file)
--- 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 1530bae72442447e39b951476482adf0512fd6b8..d6d6aefc4dee6b95ff52b75553f727abbf01775b 100644 (file)
--- 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 933d2bb51247aae2cb974edb2722ca8e192e6b08..db22851e43efc68567391c6df7c82409e0dbcd9d 100644 (file)
--- 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 6d1135a2303a3232fa5e82358b8752fc51dc8738..b3fbd5906d94123fc5ce6daf8d2e29568cbfab62 100644 (file)
--- 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 (file)
index b113664..0000000
--- 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 (file)
index 883586c..0000000
--- 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 d5cad512a825109bb03f4c9138cb111e126eb84e..9dc930f1811993c75dd8b8b19596b8c46f235827 100644 (file)
--- 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 89986ead7e0cd01a6600758bcf5369a3b309017c..e8b80d25b8d2cdc69ad8d95228499ef2a0a61fa1 100644 (file)
--- 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 199b041576550d2a1b952dd96e5ef2112087238d..f52db24a6bcb72fad797b6b061c8b430ab33857b 100644 (file)
--- 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 5886c2467042b258dbf1af3b173be9244e231ee4..3c3d421a5f69b8065b0e435aafc53420520d056d 100644 (file)
--- 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 b126df3a114ce7bffe75c42cddadf0efff88a45c..03ea56beb14a536f82747be7362ba0c348cf3c97 100644 (file)
--- 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 6a2dccb91a96c97bcff3d6b014eae8f8f5e0b708..42034c1a880a785c38402757bceca72abc41c862 100644 (file)
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -66,9 +66,7 @@ let main () =
     "<file> 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)
+;;