X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=7bc3a1b7e1006696a92509e2829140d77ac786cf;hb=c780c9756b67d116b1d5b5149ae758fa613c5fe6;hp=ee7a2eae582be1b6b4569650162d13f3cb7561c8;hpb=3c7cfd710f472bd56ba430cac8d2fa794eaecfe3;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index ee7a2eae5..7bc3a1b7e 100644
--- 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 "OK" else "FAIL" in
+    let rc,rcascii = 
+      if rc then "OK","Ok" else "FAIL","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 = 
@@ -220,3 +222,32 @@ 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 target_of mafile = 
+      let _,baseuri,_ = Librarian.baseuri_of_script 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 -> 
+        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;;
+  end 
+
+module Make = Make.Make(F) 
+