From: Enrico Tassi Date: Fri, 11 Jan 2008 19:05:05 +0000 (+0000) Subject: Make does not even try to build files that would be compiled in read-only X-Git-Tag: make_still_working~5678 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa665248454b1dcaf8cfe622dc1a159602119708;p=helm.git Make does not even try to build files that would be compiled in read-only baseuris --- diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index bab6dd2bc..376c80649 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -79,6 +79,16 @@ let find_root_for ~include_paths file = raise (NoRootFor file) ;; +let mk_baseuri root extra = + let chop name = + assert(Filename.check_suffix name ".ma" || + Filename.check_suffix name ".mma"); + try Filename.chop_extension name + with Invalid_argument "Filename.chop_extension" -> name + in + remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra)) +;; + 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 @@ -92,16 +102,9 @@ let baseuri_of_script ~include_paths file = | _ -> raise (NoRootFor (file ^" "^path^" "^root)) in let extra_buri = substract lpath lroot in - let chop name = - assert(Filename.check_suffix name ".ma" || - Filename.check_suffix name ".mma"); - try Filename.chop_extension name - with Invalid_argument "Filename.chop_extension" -> name - in let extra = String.concat "/" extra_buri in root, - remove_trailing_slash (HExtlib.normalize_path - (buri ^ "/" ^ chop extra)), + mk_baseuri buri extra, path, extra ;; @@ -146,6 +149,7 @@ module type Format = options -> source_object -> string option * 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 end module Make = functor (F:Format) -> struct @@ -283,17 +287,24 @@ module Make = functor (F:Format) -> struct purge_unwanted_roots wanted (newroots @ rest) ;; + let is_not_ro (opts,_,_) (f,_,r,_) = + match r with + | Some root -> not (F.is_readonly_buri_of opts f) + | None -> assert false + ;; + let rec make_aux root (lo,_,ct as opts) compiled failed deps = let todo = List.filter (is_buildable opts compiled deps) deps in let todo = List.filter (fun (f,_,_,_)->not (List.mem f failed)) todo in + let todo = + let local, remote = + List.partition (fun (_,_,froot,_) -> froot = Some root) todo + in + let local = List.filter (is_not_ro opts) local in + remote @ local + in if todo <> [] then let compiled, failed = - let todo = - let local, remote = - List.partition (fun (_,_,froot,_) -> froot = Some root) todo - in - remote @ local - in List.fold_left (fun (c,f) (file,_,froot,tgt) -> let rc = diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli index 0db8a83ef..63c900036 100644 --- a/helm/software/components/library/librarian.mli +++ b/helm/software/components/library/librarian.mli @@ -2,7 +2,6 @@ exception NoRootFor of string val absolutize: string -> string -val find_root: string -> string val load_root_file: string -> (string*string) list (* baseuri_of_script ?(inc:REG[matita.includes]) fname @@ -13,6 +12,8 @@ val load_root_file: string -> (string*string) list val baseuri_of_script: include_paths:string list -> string -> string * string * string * string +val mk_baseuri: string -> string -> string + (* finds all the roots files in the specified dir *) val find_roots_in_dir: string -> string list @@ -31,6 +32,7 @@ module type Format = options -> source_object -> string option * 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 end module Make : diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 97d74fdc4..6199bd5aa 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -276,7 +276,8 @@ endif ln -fs matita $(WHERE)/$$p;\ done $(H)cp -a library/ $(WHERE)/ma/standard-library - #$(H)cp -a contribs/ $(WHERE)/ma/ + $(H)M=$$PWD/matitadep cd $(WHERE)/ma/standard-library; $$M + $(H)touch install_preliminaries.stamp uninstall: diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index c14e5e3a6..91d3a81f1 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -112,6 +112,7 @@ let compile options fname = let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in + if Http_getter_storage.is_read_only baseuri then assert false; let grafite_status = GrafiteSync.init baseuri in let lexicon_status = CicNotation2.load_notation ~include_paths:[] @@ -129,9 +130,6 @@ let compile options fname = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in - if Http_getter_storage.is_read_only baseuri then - HLog.error - (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); (* cleanup of previously compiled objects *) if (not (Http_getter_storage.is_empty ~local:true baseuri) || LibraryClean.db_uris_of_baseuri baseuri <> []) @@ -150,11 +148,7 @@ let compile options fname = let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in print_string s; flush stdout); (* we dalay this error check until we print 'matitac file ' *) - if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin - HLog.error ("Baseuri "^baseuri^" not cleaned! (probably readonly)"); - (* Ugly hack *) - raise Sys.Break - end; + assert (Http_getter_storage.is_empty ~local:true baseuri); (* create dir for XML files *) if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" ~default:false) @@ -263,6 +257,11 @@ module F = let string_of_source_object s = s;; let string_of_target_object s = s;; + let is_readonly_buri_of opts file = + let buri = List.assoc "baseuri" opts in + Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file) + ;; + let root_and_target_of opts mafile = try let include_paths = get_include_paths opts in