From c81b4f59a7f58dc1e6c3ea1fc792bcce6234f866 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 1 May 2009 16:40:29 +0000 Subject: [PATCH] - librarian: 3 bugs fixed in the building system: 1) external dependences must be built using the path relative to their baseuri 2) the path of a non-existent .ma generated by a .mma was wrong 3) the compilation status of external dependences must be cached as for the other files in order to avoid looping. Repetition of failed compilation remains for dependences of external dependences because the the external compilation caches are lost in the building process When a devel is entered or leaved, its baseuei is printed for reference. This helps to disambiguate the files with the same name (eg original and reconstructed) We hope that this will not bother the tests collection mechanism. - core_notation: notation for non-functional exists had the wrong precedence - procedural/library/Makefile: -onepass was added by mistake: datatypes/bool.ma fails with -onepass because of the ambiguity of the /\ notation --- helm/software/components/library/librarian.ml | 224 ++++++------------ .../software/components/library/librarian.mli | 7 +- .../contribs/procedural/library/Makefile | 2 +- helm/software/matita/core_notation.moo | 8 +- helm/software/matita/matitacLib.ml | 6 +- 5 files changed, 82 insertions(+), 165 deletions(-) diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index 62a8a892c..2c2ba6ff2 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -23,12 +23,12 @@ * http://helm.cs.unibo.it/ *) -let debug = ref false +let debug = ref 0 let time_stamp = let old = ref 0.0 in fun msg -> - if !debug then begin + if !debug > 0 then begin let times = Unix.times () in let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in let lap = stamp -. !old in @@ -88,10 +88,24 @@ let load_root_file rootpath = lines ;; -let rec find_root_for ~include_paths file = - let include_paths = "" :: Sys.getcwd () :: include_paths in - try - let path = HExtlib.find_in include_paths file in +let find_root_for ~include_paths file = + let include_paths = "" :: Sys.getcwd () :: include_paths in + let rec find_path_for file = + try HExtlib.find_in include_paths file + with Failure "find_in" -> + if Filename.check_suffix file ".ma" then begin + let mma = Filename.chop_suffix file ".ma" ^ ".mma" in + HLog.warn ("We look for: " ^ mma); + let path = find_path_for mma in + Filename.chop_suffix path ".mma" ^ ".ma" + end else begin + HLog.error ("We are in: " ^ Sys.getcwd ()); + HLog.error ("Unable to find: "^file^"\nPaths explored:"); + List.iter (fun x -> HLog.error (" - "^x)) include_paths; + raise (NoRootFor file) + end + in + let path = find_path_for file in let path = absolutize path in (* HLog.debug ("file "^file^" resolved as "^path); *) let rootpath, root, buri = @@ -111,17 +125,7 @@ let rec find_root_for ~include_paths file = if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path - with Failure "find_in" -> - if Filename.check_suffix file ".ma" then begin - let mma = Filename.chop_suffix file ".ma" ^ ".mma" in - HLog.warn ("We look for: " ^ mma); - find_root_for ~include_paths mma - end else begin - HLog.error ("We are in: " ^ Sys.getcwd ()); - HLog.error ("Unable to find: "^file^"\nPaths explored:"); - List.iter (fun x -> HLog.error (" - "^x)) include_paths; - raise (NoRootFor file) - end + ;; let mk_baseuri root extra = @@ -192,8 +196,8 @@ module type Format = val build: options -> source_object -> bool val root_and_target_of: options -> source_object -> - (* root, writeable target, read only target *) - string option * target_object * target_object + (* root, relative source, writeable target, read only target *) + string option * source_object * 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 @@ -204,17 +208,17 @@ module Make = functor (F:Format) -> struct type status = Done of bool | Ready of bool - let say s = if !debug then prerr_endline ("make: "^s);; + let say s = if !debug > 0 then prerr_endline ("make: "^s);; let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; 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); -*) + + if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a); + if !debug > 1 then 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 @@ -232,16 +236,16 @@ module Make = functor (F:Format) -> struct | Some a, Some b -> a <= b | _ -> false in -(* - time_stamp ("L s_t: " ^ string_of_bool r); -*) + + if !debug > 1 then 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); -*) + + if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a); + if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b); + let a = try match Hashtbl.find ct a with @@ -268,126 +272,38 @@ 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); -*) + + if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a); + if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b); + a <= b | _ -> false in -(* - time_stamp ("L t_t: " ^ string_of_bool r); -*) + + if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r); + r let rec purge_unwanted_roots wanted deps = let roots, rest = List.partition - (fun (t,d,_,_) -> - not (List.exists (fun (_,d1,_,_) -> List.mem t d1) deps)) + (fun (t,_,d,_,_) -> + not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps)) deps in - let newroots = List.filter (fun (t,_,_,_) -> List.mem t wanted) roots in + let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in if newroots = roots then deps else purge_unwanted_roots wanted (newroots @ rest) ;; - let is_not_ro (opts,_,_,_,_) (f,_,r,_) = + let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = match r with | Some root -> not (F.is_readonly_buri_of opts f) | None -> assert false ;; -(* FG: Old sorting algorithm ************************************************) -(* - let rec get_status opts what = - let _, _, _, cc, cd = opts in - let t, dependencies, root, tgt = what in - try Done (Hashtbl.find cc t) -(* say "already built" *) - with Not_found -> - let map st d = match st with - | Done false -> st - | Ready false -> st - | _ -> - let whatd = Hashtbl.find cd d in - let _, _, _, tgtd = whatd in - begin match st, get_status opts whatd with - | _, Done false -> Hashtbl.add cc t false; Done false - | Done true, Done true -> - if modified_before_t_t opts tgt tgtd then Ready true else Done true -(* say (F.string_of_source_object t^" depends on "^F.string_of_target_object unsat^" and "^F.string_of_source_object t^".o is younger than "^ F.string_of_target_object unsat^", thus needs to be built") *) - | Done true, Ready _ -> Ready false - | Ready true, Ready _ -> Ready false -(* say (F.string_of_source_object t^" depends on "^ F.string_of_source_object (fst4 unsat)^ " that is not built, thus is not ready") *) - | Ready true, Done true -> Ready true - | _ -> st - end - in - let st = if modified_before_s_t opts t tgt then Done true else Ready true in - match List.fold_left map st dependencies with - | Done true -> Hashtbl.add cc t true; Done true -(* say(F.string_of_source_object t^" is built" *) - | st -> st - - let list_partition_filter_rev filter l = - let rec aux l1 l2 = function - | [] -> l1, l2 - | hd :: tl -> - begin match filter hd with - | None -> aux l1 l2 tl - | Some true -> aux (hd :: l1) l2 tl - | Some false -> aux l1 (hd :: l2) tl - end - in - aux [] [] l - - let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps = - time_stamp "filter get_status: begin"; - let map what = match get_status opts what with - | Done _ -> None - | Ready b -> Some b - in - let todo, deps = list_partition_filter_rev map deps in - time_stamp "filter get_status: end"; - let todo = - let local, remote = - List.partition (fun (_,_,froot,_) -> froot = Some root) todo - in - let local, skipped = List.partition (is_not_ro opts) local in - List.iter - (fun x -> - HLog.warn("Read only baseuri for: "^F.string_of_source_object(fst4 x))) - skipped; - remote @ local - in - if todo <> [] then begin - let ok = List.fold_left - (fun ok (file,_,froot,tgt) -> - let rc = - match froot with - | Some froot when froot = root -> - Hashtbl.remove ct tgt; - Hashtbl.add ct tgt None; - time_stamp "building"; - let r = F.build lo file in - time_stamp "done"; r - | Some froot -> make froot [file] - | None -> - HLog.error ("No root for: "^F.string_of_source_object file); - false - in - Hashtbl.add cc file rc; - ok && rc - ) - ok (List.rev todo) - in - make_aux root opts ok (List.rev deps) - end - else - ok -*) + (* FG: new sorting algorithm ************************************************) let rec make_aux root opts ok deps = @@ -395,10 +311,10 @@ module Make = functor (F:Format) -> struct and make_one root opts ok what = let lo, _, ct, cc, cd = opts in - let t, deps, froot, tgt = what in + let t, path, deps, froot, tgt = what in let str = F.string_of_source_object t in let map (okd, okt) d = - let (_, _, _, tgtd) as whatd = (Hashtbl.find cd d) in + let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in let r = make_one root opts okd whatd in r, okt && modified_before_t_t opts tgtd tgt in @@ -413,22 +329,20 @@ module Make = functor (F:Format) -> struct let res = if okd then if okt then true else - match froot with + let build path = match froot with | Some froot when froot = root -> - if is_not_ro opts what then begin - Hashtbl.remove ct tgt; - Hashtbl.add ct tgt None; - time_stamp ("L : BUILDING " ^ str); - let res = F.build lo t in - time_stamp ("L : DONE " ^ str); res - end else begin - 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 -> - HLog.error ("No root for: " ^ str); false + if is_not_ro opts what then F.build lo path else + (HLog.error ("Read only baseuri for: " ^ str ^ + ", I won't compile it even if it is out of date"); + false) + | Some froot -> make froot [path] + | None -> HLog.error ("No root for: " ^ str); false + in + Hashtbl.remove ct tgt; + Hashtbl.add ct tgt None; + time_stamp ("L : BUILDING " ^ str); + let res = build path in + time_stamp ("L : DONE " ^ str); res else false in time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); @@ -443,6 +357,8 @@ module Make = functor (F:Format) -> struct Sys.chdir root; let deps = F.load_deps_file (root^"/depends") in let local_options = load_root_file (root^"/root") in + let baseuri = List.assoc "baseuri" local_options in + print_endline ("Entering HELM directory: " ^ baseuri); flush stdout; let caches,cachet,cachec,cached = Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 in @@ -450,18 +366,18 @@ module Make = functor (F:Format) -> struct let deps = List.map (fun (file,d) -> - let r,wtgt,rotgt = F.root_and_target_of local_options file in + let r,path,wtgt,rotgt = F.root_and_target_of local_options file in Hashtbl.add caches file (F.mtime_of_source_object file); (* if a read only target exists, we use that one, otherwise we use the writeable one that may be compiled *) - let _,_,_, tgt as tuple = + let _,_,_,_, tgt as tuple = match F.mtime_of_target_object rotgt with | Some _ as mtime -> Hashtbl.add cachet rotgt mtime; - (file, d, r, rotgt) + (file, path, d, r, rotgt) | None -> Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); - (file, d, r, wtgt) + (file, path, d, r, wtgt) in Hashtbl.add cached file tuple; tuple @@ -473,9 +389,9 @@ module Make = functor (F:Format) -> struct if targets = [] then make_aux root opts true deps else - make_aux root opts true - (purge_unwanted_roots targets deps) + make_aux root opts true (purge_unwanted_roots targets deps) in + print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout; HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; time_stamp "L : LEAVING"; diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli index 0e15e28bc..4eed9051d 100644 --- a/helm/software/components/library/librarian.mli +++ b/helm/software/components/library/librarian.mli @@ -71,8 +71,8 @@ module type Format = val build: options -> source_object -> bool val root_and_target_of: options -> source_object -> - (* root, writeable target, read only target *) - string option * target_object * target_object + (* root, relative source, writeable target, read only target *) + string option * source_object * 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 @@ -99,6 +99,7 @@ val write_deps_file: string option -> (string * string list) list -> unit (* true if the argunent starts with a uri scheme prefix *) val is_uri: string -> bool -val debug: bool ref +(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *) +val debug: int ref val time_stamp: string -> unit diff --git a/helm/software/matita/contribs/procedural/library/Makefile b/helm/software/matita/contribs/procedural/library/Makefile index 0fa53112e..6d8bdcaab 100644 --- a/helm/software/matita/contribs/procedural/library/Makefile +++ b/helm/software/matita/contribs/procedural/library/Makefile @@ -1,4 +1,4 @@ DEVEL = library -MATITAOPTIONS = -no-default-includes -onepass +MATITAOPTIONS = -no-default-includes include ../Makefile.common diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index b93dd98e1..be61e6650 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -1,5 +1,9 @@ (* exists *******************************************************************) +notation "hvbox(∃ _ break . p)" + with precedence 20 +for @{'exists $p }. + notation < "hvbox(\exists ident i : ty break . p)" right associative with precedence 20 for @{'exists (\lambda ${ident i} : $ty. $p) }. @@ -8,10 +12,6 @@ notation < "hvbox(\exists ident i break . p)" with precedence 20 for @{'exists (\lambda ${ident i}. $p) }. -notation "hvbox(∃ _ break . p)" - with precedence 20 -for @{'exists $p }. - (* notation < "hvbox(\exists ident i opt (: ty) break . p)" right associative with precedence 20 diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 6c3749db3..5a14b2703 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -337,7 +337,7 @@ module F = let root_and_target_of opts mafile = try let include_paths = get_include_paths opts in - let root,baseuri,_,_ = + let root,baseuri,_,relpath = Librarian.baseuri_of_script ~include_paths mafile in let obj_writeable, obj_read_only = @@ -350,8 +350,8 @@ module F = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:false in - Some root, obj_writeable, obj_read_only - with Librarian.NoRootFor x -> None, "", "" + Some root, relpath, obj_writeable, obj_read_only + with Librarian.NoRootFor x -> None, "", "", "" ;; let mtime_of_source_object s = -- 2.39.2