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 bab6dd2bc290a66f126e442352b580843b6da24c..376c8064974c73927258ebd913d55a8b16ca001c 100644 (file)
--- 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 0db8a83ef9a7719ebde8b348d6218352d254db04..63c900036f89d92f4dd98fd0a4cdcc5195ced80e 100644 (file)
--- 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 97d74fdc4b1662661f02d006ca9ca40f429f676b..6199bd5aa9f3fada1d48799495d8e92b6ec21ade 100644 (file)
--- 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 c14e5e3a60f4bd7b9b1ed8896bf6af1a7c840c30..91d3a81f1d6e2115f93a76c9c65db40274c458d8 100644 (file)
--- 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