From 1c0a1dbfd13f0618b33213c4d42e50d44465c987 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 17 Apr 2015 15:36:11 +0200 Subject: Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several libraries at once (see #4193). --- library/library.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 9d0ccb972a..b4261309fd 100644 --- a/library/library.ml +++ b/library/library.ml @@ -633,7 +633,12 @@ let import_module export modl = with Not_found-> flush acc; safe_locate_module m, [] in (match m with | MPfile dir -> aux (dir::acc) l - | mp -> flush acc; Declaremods.import_module export mp; aux [] l) + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err_loc (loc,"import_library", + str ((string_of_qualid dir)^" is not a module"))) | [] -> flush acc in aux [] modl -- cgit v1.2.3 From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 22 Apr 2015 18:51:48 +0200 Subject: Tactical `progress` compares term up to potentially equalisable universes. Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.--- library/universes.ml | 66 +++++++++++++++++++++++++++++++++++---------------- library/universes.mli | 8 +++++++ 2 files changed, 54 insertions(+), 20 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 9fddc7067b..3a8ee26254 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n = let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in res, !cstrs +(** Variant of [eq_constr_univs_infer] taking kind-of-term functions, + to expose subterms of [m] and [n], arguments. *) +let eq_constr_univs_infer_with kind1 kind2 univs m n = + (* spiwack: duplicates the code of [eq_constr_univs_infer] because I + haven't find a way to factor the code without destroying + pointer-equality optimisations in [eq_constr_univs_infer]. + Pointer equality is not sufficient to ensure equality up to + [kind1,kind2], because [kind1] and [kind2] may be different, + typically evaluating [m] and [n] in different evar maps. *) + let cstrs = ref Constraints.empty in + let eq_universes strict = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if Univ.check_eq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, UEq, u2) !cstrs; + true) + in + let rec eq_constr' m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + res, !cstrs + let leq_constr_univs_infer univs m n = if m == n then true, Constraints.empty else @@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; + true) in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + if Univ.check_leq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, ULe, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n = eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + res, !cstrs let eq_constr_universes m n = if m == n then true, Constraints.empty @@ -188,7 +214,7 @@ let eq_constr_universes m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + res, !cstrs let leq_constr_universes m n = if m == n then true, Constraints.empty @@ -216,22 +242,22 @@ let leq_constr_universes m n = Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + res, !cstrs let compare_head_gen_proj env equ eqs eqc' m n = match kind_of_term m, kind_of_term n with | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> - (match kind_of_term f with - | Const (p', u) when eq_constant (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then - eqc' c args.(npars) - else false - | _ -> false) + (match kind_of_term f with + | Const (p', u) when eq_constant (Projection.constant p) p' -> + let pb = Environ.lookup_projection p env in + let npars = pb.Declarations.proj_npars in + if Array.length args == npars + 1 then + eqc' c args.(npars) + else false + | _ -> false) | _ -> Constr.compare_head_gen equ eqs eqc' m n - + let eq_constr_universes_proj env m n = if m == n then true, Constraints.empty else @@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n = m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n in let res = eq_constr' m n in - res, !cstrs + res, !cstrs (* Generator of levels *) let new_univ_level, set_remote_new_univ_level = diff --git a/library/universes.mli b/library/universes.mli index 252648d7dc..5527da0903 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints application grouping, the universe constraints in [u] and additional constraints [c]. *) val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of + {!eq_constr_univs_infer} taking kind-of-term functions, to expose + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr,types) kind_of_term) -> + (constr -> (constr,types) kind_of_term) -> + Univ.universes -> constr -> constr -> bool universe_constrained + (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -- cgit v1.2.3 From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Apr 2015 14:55:11 +0200 Subject: Remove almost all the uses of string concatenation when building error messages. Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. --- library/declaremods.ml | 2 +- library/goptions.ml | 16 +++++++++------- library/impargs.ml | 7 +++++-- library/lib.ml | 11 +++++++---- library/libobject.ml | 5 ++--- library/library.ml | 29 ++++++++++++++--------------- 6 files changed, 38 insertions(+), 32 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index cc7c4d7f11..a82f5260ba 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -950,7 +950,7 @@ type 'modast module_params = let debug_print_modtab _ = let pr_seg = function | [] -> str "[]" - | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") + | l -> str "[." ++ int (List.length l) ++ str ".]" in let pr_modinfo mp (prefix,substobjs,keepobjs) s = s ++ str (string_of_mp mp) ++ (spc ()) diff --git a/library/goptions.ml b/library/goptions.ml index ef25fa5902..4f50fbfbdd 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -35,7 +35,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - error ((nickname key)^": no table or option of this type") + errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) @@ -301,7 +301,9 @@ let declare_string_option = let set_option_value locality check_and_cast key v = let (name, depr, (_,read,write,lwrite,gwrite)) = try get_option key - with Not_found -> error ("There is no option "^(nickname key)^".") + with Not_found -> + errorlabstrm "Goptions.set_option_value" + (str "There is no option " ++ str (nickname key) ++ str ".") in let write = match locality with | None -> write @@ -364,9 +366,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg_info (str ("The "^name^" mode is "^(if b then "on" else "off"))) + msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) + msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in @@ -383,7 +385,7 @@ let get_tables () = let print_tables () = let print_option key name value depr = - let msg = str (" "^(nickname key)^": ") ++ msg_option_value (name, value) in + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in @@ -401,10 +403,10 @@ let print_tables () = !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !string_table (mt ()) ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () diff --git a/library/impargs.ml b/library/impargs.ml index 4b0e2e3d1a..94f53219e7 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Globnames +open Nameops open Term open Reduction open Declarations @@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".") + errorlabstrm "" + (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - error ("Bad implicit argument number: "^(string_of_int i)^".") + errorlabstrm "" + (str "Bad implicit argument number: " ++ int i ++ str ".") else errorlabstrm "" (str "Cannot set implicit argument number " ++ int i ++ diff --git a/library/lib.ml b/library/lib.ml index 9977b66654..81db547efd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -75,7 +75,8 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - error ("there are still opened " ^ module_kind ty ^"s") + errorlabstrm "Lib.classify_segment" + (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -274,7 +275,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in errorlabstrm "" - (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") + (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -318,7 +319,8 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - error ("There are some open "^module_kind ty^"s.") + errorlabstrm "Lib.end_compilation_checks" + (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () in @@ -369,7 +371,8 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - error ("Last block to end has name "^(Names.Id.to_string id')^"."); + errorlabstrm "Lib.find_opening_node" + (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." diff --git a/library/libobject.ml b/library/libobject.ml index 5f2a2127d9..74930d76ec 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -7,6 +7,7 @@ (************************************************************************) open Libnames +open Pp (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -33,15 +34,13 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -let yell s = Errors.anomaly (Pp.str s) - let default_object s = { object_name = s; cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); subst_function = (fun _ -> - yell ("The object "^s^" does not know how to substitute!")); + Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} diff --git a/library/library.ml b/library/library.ml index b4261309fd..1ffa1a305c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -126,7 +126,8 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (DirPath.to_string dir)) + errorlabstrm "Library.find_library" + (str "Unknown library " ++ str (DirPath.to_string dir)) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -378,10 +379,10 @@ let access_table what tables dp i = let t = try fetch_delayed f with Faulty f -> - error - ("The file "^f^" (bound to " ^ dir_path ^ - ") is inaccessible or corrupted,\n" ^ - "cannot load some "^what^" in it.\n") + errorlabstrm "Library.access_table" + (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ + str ") is inaccessible or corrupted,\ncannot load some " ++ + str what ++ str " in it.\n") in tables := LibraryMap.add dp (Fetched t) !tables; t @@ -462,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); @@ -475,9 +476,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (try_locate_absolute_library dir) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ - ".vo makes inconsistent assumptions over library " ^ - DirPath.to_string dir)); + errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); libs let rec_intern_library libs mref = @@ -487,7 +486,7 @@ let rec_intern_library libs mref = let check_library_short_name f dir = function | Some id when not (Id.equal id (snd (split_dirpath dir))) -> errorlabstrm "check_library_short_name" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ pr_id id) | _ -> () @@ -613,7 +612,7 @@ let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> user_err_loc - (loc,"import_library", str (string_of_qualid qid ^ " is not a module")) + (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -638,7 +637,7 @@ let import_module export modl = try Declaremods.import_module export mp; aux [] l with Not_found -> user_err_loc (loc,"import_library", - str ((string_of_qualid dir)^" is not a module"))) + str (string_of_qualid dir) ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -650,8 +649,8 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^ - ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) + (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain others caracters than letters, digits, or `_` *) @@ -795,7 +794,7 @@ let save_library_to ?todo dir f otab = msg_error (str"Could not compile the library to native code. Skipping.") with reraise -> let reraise = Errors.push reraise in - let () = msg_warning (str ("Removed file "^f')) in + let () = msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise -- cgit v1.2.3