From 6f2db13c8677fd0148279483359e75b9f128aebc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 7 Jul 2015 16:02:13 +0200 Subject: Univs/minimization: Fix unused variable bug. --- library/universes.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index a3926bc6f2..1c8a5ad77d 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -723,7 +723,10 @@ let pr_constraints_map cmap = prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () ++ acc) cmap (mt ()) - + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> @@ -767,8 +770,8 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in - instantiate_with_lbound u lbound false false acc + let acc' = remove_alg l acc in + instantiate_with_lbound u lbound false false acc' else acc, (true, false, lbound) | None -> try -- cgit v1.2.3 From 26911bbc0bb3347c922d12b07a1c2bc34bba3c8d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 9 Jul 2015 13:55:36 +0200 Subject: Improve semantics of -native-compiler flag. Since Guillaume's, launching coqtop without -native-compiler and call native_compute would mean recompiling silently all dependencies, even if they had been precompiled (e.g. the stdlib). The new semantics is that -native-compiler disables separate compilation of the current library, but still tries to load precompiled dependencies. If loading fails when the flag is on, coqtop stays silent. --- library/library.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index a8fbe0841c..45fce1c26c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -169,8 +169,9 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if !Flags.native_compiler then - Nativelib.link_library ~prefix ~dirname ~basename:f + (* This will not produce errors or warnings if the native compiler was + not enabled *) + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] -- cgit v1.2.3 From c4486dfda07b872d20746778df5c443b052b92b9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 9 Jul 2015 21:08:44 +0200 Subject: Native compiler: refactor code handling pre-computed values. Fixes #4139 (Not_found exception with Require in modules). --- library/declaremods.ml | 10 +++------- library/declaremods.mli | 2 +- library/global.mli | 2 +- 3 files changed, 5 insertions(+), 9 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index a82f5260ba..f66656d09a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects (** For the native compiler, we cache the library values *) -type library_values = Nativecode.symbol array -let library_values = - Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" - let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = @@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv univ digest in + let mp' = Global.import cenv univ digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); - library_values := Dirmap.add dir values !library_values in let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs -let get_library_symbols_tbl dir = Dirmap.find dir !library_values +let get_library_native_symbols dir = + Safe_typing.get_library_native_symbols (Global.safe_env ()) dir let start_library dir = let mp = Global.start_library dir in diff --git a/library/declaremods.mli b/library/declaremods.mli index c3578ec421..319d168d05 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -75,7 +75,7 @@ val register_library : Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.universe_context_set -> unit -val get_library_symbols_tbl : library_name -> Nativecode.symbol array +val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit diff --git a/library/global.mli b/library/global.mli index 248e1f86dd..75a1ebee94 100644 --- a/library/global.mli +++ b/library/global.mli @@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path * Nativecode.symbol array + module_path (** {6 Misc } *) -- cgit v1.2.3 From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:59 +0200 Subject: Option -type-in-type: added support in checker and making it contaminating in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk? --- library/global.ml | 1 - library/global.mli | 1 - 2 files changed, 2 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 49fa2ef28f..0419799b67 100644 --- a/library/global.ml +++ b/library/global.ml @@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) -let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 75a1ebee94..363bb57890 100644 --- a/library/global.mli +++ b/library/global.mli @@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit -val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) -- cgit v1.2.3 From 93579407f5795c117d6c6f1399396b690f80d723 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 09:32:36 +0200 Subject: Fixing anomaly #3743 while printing an error message involving evar constraints. Indeed, the name of a bound variable was lost when unifying under a Prod in evarconv. The error message for "Unable to satisfy the following constraints" is still to be improved though. --- library/nameops.ml | 5 +++++ library/nameops.mli | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/nameops.ml b/library/nameops.ml index 02b085a7ac..3a23ab97df 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -136,6 +136,11 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous +let name_max na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + let pr_lab l = str (Label.to_string l) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nameops.mli b/library/nameops.mli index 23432ae2fa..de1f99fe0f 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit val name_cons : Name.t -> Id.t list -> Id.t list val name_app : (Id.t -> Id.t) -> Name.t -> Name.t val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - +val name_max : Name.t -> Name.t -> Name.t val pr_lab : Label.t -> Pp.std_ppcmds -- cgit v1.2.3