librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 4c222b0b936692fa0d22a76f0d0739c861f195dd..62a8a892c3887f5b965266e49077846456ffa227 100644 (file)
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -191,7 +191,9 @@ module type Format =
     val string_of_target_object: target_object -> string
     val build: options -> source_object -> bool
     val root_and_target_of: 
-          options -> source_object -> string option * target_object
+          options -> source_object -> 
+          (* root, writeable target, read only target *)
+          string option * target_object * target_object
     val mtime_of_source_object: source_object -> float option
     val mtime_of_target_object: target_object -> float option
     val is_readonly_buri_of: options -> source_object -> bool
@@ -209,10 +211,10 @@ module Make = functor (F:Format) -> struct
   let fst4 = function (x,_,_,_) -> x;;
 
   let modified_before_s_t (_,cs, ct, _, _) a b = 
-(*    
+(*   
     time_stamp ("L s_t: a " ^ F.string_of_source_object a);
     time_stamp ("L s_t: b " ^ F.string_of_target_object b);
-*)
+*)    
     let a = try Hashtbl.find cs a with Not_found -> assert false in
     let b = 
       try
@@ -230,16 +232,16 @@ module Make = functor (F:Format) -> struct
        | Some a, Some b -> a <= b
        | _ -> false
     in
-(*    
+(*
     time_stamp ("L s_t: " ^ string_of_bool r);
-*)    
+*)
     r
 
   let modified_before_t_t (_,_,ct, _, _) a b =
-(*    
+(*
     time_stamp ("L t_t: a " ^ F.string_of_target_object a);
     time_stamp ("L t_t: b " ^ F.string_of_target_object b);
-*) 
+*)    
     let a = 
       try
         match Hashtbl.find ct a with
@@ -266,16 +268,16 @@ module Make = functor (F:Format) -> struct
     in
     let r = match a, b with
        | Some a, Some b ->
-(*       
+(*
        time_stamp ("tt: a " ^ string_of_float a);
        time_stamp ("tt: b " ^ string_of_float b);
-*)       
+*)
           a <= b
        | _ -> false
     in
-(*    
+(*
     time_stamp ("L t_t: " ^ string_of_bool r);
-*)    
+*)
     r
 
   let rec purge_unwanted_roots wanted deps =
@@ -420,10 +422,9 @@ module Make = functor (F:Format) -> struct
                   let res = F.build lo t in
                   time_stamp ("L : DONE     " ^ str); res
                end else begin
-                   Hashtbl.remove ct tgt;
-                   Hashtbl.add ct tgt None;
-                  HLog.warn("Read only baseuri for: "^ str^
-                     ", assuming it is aleary built."); true
+                  HLog.error ("Read only baseuri for: "^ str^
+                     ", I won't compile it even if it is out of date"); 
+                  false
                end
              | Some froot -> make froot [t]
              | None -> 
@@ -449,11 +450,21 @@ module Make = functor (F:Format) -> struct
     let deps = 
       List.map 
         (fun (file,d) -> 
-          let r,tgt = F.root_and_target_of local_options file in
+          let r,wtgt,rotgt = F.root_and_target_of local_options file in
           Hashtbl.add caches file (F.mtime_of_source_object file);
-          Hashtbl.add cachet tgt (F.mtime_of_target_object tgt); 
-          Hashtbl.add cached file (file, d, r, tgt);
-          (file, d, r, tgt)
+         (* if a read only target exists, we use that one, otherwise
+            we use the writeable one that may be compiled *)
+         let _,_,_, tgt as tuple = 
+           match F.mtime_of_target_object rotgt with
+           | Some _ as mtime ->
+               Hashtbl.add cachet rotgt mtime; 
+              (file, d, r, rotgt)
+           | None -> 
+               Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); 
+              (file, d, r, wtgt)
+         in
+          Hashtbl.add cached file tuple;
+          tuple
        )
         deps
     in

diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli
index f448e52b554f72e9578cf95261d0a5e7a789ee62..0e15e28bcc78dc5b88bdff6bc208e22d4939d23e 100644 (file)
--- a/helm/software/components/library/librarian.mli
+++ b/helm/software/components/library/librarian.mli
@@ -70,7 +70,9 @@ module type Format =
     val string_of_target_object: target_object -> string
     val build: options -> source_object -> bool
     val root_and_target_of: 
-          options -> source_object -> string option * target_object
+          options -> source_object -> 
+          (* root, writeable target, read only target *)
+          string option * target_object * target_object
     val mtime_of_source_object: source_object -> float option
     val mtime_of_target_object: target_object -> float option
     val is_readonly_buri_of: options -> source_object -> bool

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 70ed5766d273f35db6dbf293aa5313519993faac..f248545fba8c6d5caae409eb43fee604273185b2 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -357,15 +357,18 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-        let obj =
+        let obj_writeable, obj_read_only =
            if Filename.check_suffix mafile ".mma" then 
+              Filename.chop_suffix mafile ".mma" ^ ".ma",
               Filename.chop_suffix mafile ".mma" ^ ".ma"
            else
               LibraryMisc.obj_file_of_baseuri 
-                        ~must_exist:false ~baseuri ~writable:true
+                        ~must_exist:false ~baseuri ~writable:true,
+              LibraryMisc.obj_file_of_baseuri 
+                        ~must_exist:false ~baseuri ~writable:false
         in
-        Some root, obj 
-      with Librarian.NoRootFor x -> None, ""
+        Some root, obj_writeable, obj_read_only
+      with Librarian.NoRootFor x -> None, "", ""
     ;;
 
     let mtime_of_source_object s =