huge amount of work to make out Make crawl roots and

[helm.git] / matita / matitacLib.ml

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 80e81c2d7386f647b10c94aed0f4016dc6ae22ab..3c3d421a5f69b8065b0e435aafc53420520d056d 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -69,7 +69,8 @@ let pp_times fname rc big_bang =
     let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
     let r = Unix.gettimeofday () -. big_bang in
     let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
-    let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
+    let rc,rcascii = 
+      if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
     let times = 
       let fmt t = 
         let seconds = int_of_float t in
@@ -82,7 +83,8 @@ let pp_times fname rc big_bang =
     in
     let s = Printf.sprintf "%-4s %s %s" rc times extra in
     print_endline s;
-    flush stdout
+    flush stdout;
+    HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
 ;;
 
 let cut prefix s = 
@@ -93,16 +95,25 @@ let cut prefix s =
   String.sub s lenp (lens-lenp)
 ;;
 
-let rec compile fname =
-  Helm_registry.set_string "matita.filename" 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 root,baseuri,fname = Librarian.baseuri_of_script ~include_paths fname in
+  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
   in
@@ -203,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);
@@ -221,3 +232,46 @@ let rec compile fname =
        clean_exit baseuri false
 ;;
 
+module F = 
+  struct 
+    type source_object = string
+    type target_object = string
+    let string_of_source_object s = s;;
+    let string_of_target_object s = s;;
+
+    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 
+    ;;
+
+    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 -> 
+              None
+(*         max_float *)
+(*         raise (Failure ("Unable to stat a source file: " ^ s))  *)
+    ;;
+
+    let mtime_of_target_object s =
+      try Some (Unix.stat s).Unix.st_mtime
+      with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+    ;;
+
+    let build = compile;;
+
+    let load_deps_file = Librarian.load_deps_file;;
+
+  end 
+
+module Make = Librarian.Make(F) 
+