From 7a3c40d0d56ba3c20126f1d2c9f651adc95eaef7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 30 Sep 2008 10:42:43 +0000 Subject: [PATCH] librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than before) --- helm/software/components/library/librarian.ml | 49 ++++++++++++------- .../software/components/library/librarian.mli | 4 +- helm/software/matita/matitacLib.ml | 11 +++-- 3 files changed, 40 insertions(+), 24 deletions(-) diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index 4c222b0b9..62a8a892c 100644 --- 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 f448e52b5..0e15e28bc 100644 --- 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 70ed5766d..f248545fb 100644 --- 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 = -- 2.39.2