From 55ce331822a673d710451c628ec5a731ab36da1f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 2 Feb 2016 15:28:48 +0100 Subject: Fix bug #4544: Backtrack on using full betaiota reduction during keyed unification. --- tactics/equality.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index ef1ec13ba..80f6038cb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -228,8 +228,8 @@ let rewrite_keyed_core_unif_flags = { (* This is set dynamically *) restrict_conv_on_strict_subterms = false; - modulo_betaiota = true; - (* Different from conv_closed *) + modulo_betaiota = false; + modulo_eta = true; } -- cgit v1.2.3 From 5bca0e81c46c1cc6427f939263670996f570dbcf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 2 Feb 2016 15:47:23 +0100 Subject: Fix part of bug #4533: respect declared global transparency of projections in unification.ml --- pretyping/unification.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6cb1bc702..55210d067 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -481,7 +481,8 @@ let key_of env b flags f = Id.Pred.mem id (fst flags.modulo_delta) -> Some (IsKey (VarKey id)) | Proj (p, c) when Projection.unfolded p - || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) -> + || (is_transparent env (ConstKey (Projection.constant p)) && + (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) -> Some (IsProj (p, c)) | _ -> None -- cgit v1.2.3 From e7b292de756b335069fce9d9a999904ea2af6630 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Feb 2016 18:21:02 +0100 Subject: Document differences of Hint Resolve and Hint Extern --- test-suite/success/auto.v | 89 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index aaa7b3a51..5477c8331 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -45,3 +45,92 @@ Proof. eexists. Fail progress debug eauto with test2. progress eauto with test. Qed. + +(** Patterns of Extern have a "matching" semantics. + It is not so for apply/exact hints *) + +Class B (A : Type). +Class I. +Instance i : I. + +Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y. +Class D (f : nat -> nat -> nat). +Definition ftest (x y : nat) := x + y. +Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f). + Admitted. +Module Instnopat. + Local Instance: B nat. + (* pattern_of_constr -> B nat *) + (* exact hint *) + Check (_ : B nat). + (* map_eauto -> B_instance0 *) + (* NO Constr_matching.matches !!! *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + eauto with typeclass_instances. + Qed. + + Local Instance: D ftest. + Local Hint Resolve flipD | 0 : typeclass_instances. + (* pattern: D (flip _) *) + Fail Timeout 1 Check (_ : D _). (* loops applying flipD *) + +End Instnopat. + +Module InstnopatApply. + Local Instance: I -> B nat. + (* pattern_of_constr -> B nat *) + (* apply hint *) + Check (_ : B nat). + (* map_eauto -> B_instance0 *) + (* NO Constr_matching.matches !!! *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + eauto with typeclass_instances. + Qed. +End InstnopatApply. + +Module InstPat. + Hint Extern 3 (B nat) => split : typeclass_instances. + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> true *) + Check (_ : B nat). + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> false: + Because an inductive in the pattern does not match an evar in the goal *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + (* map_existential -> Extern hint *) + (* Constr_matching.matches -> false *) + Fail progress eauto with typeclass_instances. + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> false *) + Fail typeclasses eauto. + Abort. + + Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances. + Module withftest. + Local Instance: D ftest. + + Check (_ : D _). + (* D_instance_0 : D ftest *) + Check (_ : D (flip _)). + (* ... : D (flip ftest) *) + End withftest. + Module withoutftest. + Hint Extern 0 (D ftest) => split : typeclass_instances. + Check (_ : D _). + (* ? : D ?, _not_ looping *) + Check (_ : D (flip _)). + (* ? : D (flip ?), _not_ looping *) + + Check (_ : D (flip ftest)). + (* flipD ftest {| |} : D (flip ftest) *) + End withoutftest. +End InstPat. -- cgit v1.2.3 From 20fe4afb53e2b68ffb06a5504a444e536d4b813e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 24 Feb 2016 16:06:40 +0100 Subject: Document Hint Mode, cleanup Hint doc. --- doc/refman/RefMan-tac.tex | 40 ++++++++++++++++++---------------------- 1 file changed, 18 insertions(+), 22 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9a365b829..903e2e19a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3669,9 +3669,6 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - The cost of that hint is the number of subgoals generated by that - tactic. - % Is it really needed? %% In case the inferred type of \term\ does not start with a product %% the tactic added in the hint list is {\tt exact {\term}}. In case @@ -3869,7 +3866,25 @@ is to set the cut expression to $c | e$, the initial cut expression being \texttt{emp}. +\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid} +\label{HintMode} +\comindex{Hint Mode} + +This sets an optional mode of use of the identifier {\qualid}. When +proof-search faces a goal that ends in an application of {\qualid} to +arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the +hints associated to qualid can be applied or not. A mode specification +is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is +to be treated as an input {\tt +} or an output {\tt -} of the +identifier. For a mode to match a list of arguments, input terms \emph{must +not} contain existential variables, while outputs can be any term. +Multiple modes can be declared for a single identifier, in that case +only one mode needs to match the arguments for the hints to be applied. +{\tt Hint Mode} is especially useful for typeclasses, when one does not +want to support default instances and avoid ambiguity in +general. Setting a parameter of a class as an input forces proof-search +to be driven by that index of the class. \end{itemize} @@ -3877,25 +3892,6 @@ being \texttt{emp}. pattern-matching on hypotheses using \texttt{match goal with} inside the tactic. -\begin{Variants} -\item {\tt Hint \hintdef} - - No database name is given: the hint is registered in the {\tt core} - database. - -\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$} - - This is used to declare hints that must not be exported to the other - modules that require and import the current module. Inside a - section, the option {\tt Local} is useless since hints do not - survive anyway to the closure of sections. - -\item {\tt Hint Local \hintdef} - - Idem for the {\tt core} database. - -\end{Variants} - % There are shortcuts that allow to define several goal at once: % \begin{itemize} -- cgit v1.2.3 From db2c6f0054d3e05f82da7494ce790c04b1976401 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 28 Feb 2016 13:19:47 +0100 Subject: Fixing bug #4596: [rewrite] broke in the past few weeks. Checking that a term was indeed a relation was made too early, as the decomposition function recognized relations of the form "f (g .. (h x y)) with f, g unary and only h binary. We postpone this check to the very end. --- tactics/rewrite.ml | 8 ++++++-- test-suite/bugs/closed/4596.v | 14 ++++++++++++++ 2 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4596.v diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 5ca74050a..803e187ff 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -468,11 +468,15 @@ let rec decompose_app_rel env evd t = let len = Array.length args in let fargs = Array.sub args 0 (Array.length args - 2) in let rel = mkApp (f, fargs) in - let ty = Retyping.get_type_of env evd rel in - let () = if not (Reduction.is_arity env ty) then error_no_relation () in rel, args.(len - 2), args.(len - 1) | _ -> error_no_relation () +let decompose_app_rel env evd t = + let (rel, t1, t2) = decompose_app_rel env evd t in + let ty = Retyping.get_type_of env evd rel in + let () = if not (Reduction.is_arity env ty) then error_no_relation () in + (rel, t1, t2) + let decompose_applied_relation env sigma (c,l) = let ctype = Retyping.get_type_of env sigma c in let find_rel ty = diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v new file mode 100644 index 000000000..592fdb658 --- /dev/null +++ b/test-suite/bugs/closed/4596.v @@ -0,0 +1,14 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. + +Definition T (x : bool) := x = true. + +Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat) + (s : forall n : nat, bool) + (s0 s1 : nat -> S -> S), + (forall (str0 : S) (n m : nat), + (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) -> + T (b str0 m)) -> + T (b str p). +Proof. +intros ???????? H0. +rewrite H0. -- cgit v1.2.3 From 508d5a99101097948b6de342295eec0d5c8cbe72 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Mar 2016 18:59:51 +0100 Subject: Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. --- interp/notation.ml | 6 ++++-- lib/unicode.ml | 7 +++++++ lib/unicode.mli | 3 +++ 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af7..c4addbf10 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -314,7 +314,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = patl let mkNumeral n = Numeral n -let mkString s = String s +let mkString = function +| None -> None +| Some s -> if Unicode.is_utf8 s then Some (String s) else None let delay dir int loc x = (dir, (fun () -> int loc x)) @@ -326,7 +328,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) - (patl, (fun r -> Option.map mkString (uninterp r)), inpat) + (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () diff --git a/lib/unicode.ml b/lib/unicode.ml index 1765e93dc..cfaa73cc1 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -168,6 +168,13 @@ let next_utf8 s i = (c land 0x3F) lsl 6 + (d land 0x3F) else err () +let is_utf8 s = + let rec check i = + let (off, _) = next_utf8 s i in + check (i + off) + in + try check 0 with End_of_input -> true | Invalid_argument _ -> false + (* Check the well-formedness of an identifier *) let initial_refutation j n s = diff --git a/lib/unicode.mli b/lib/unicode.mli index 520203d43..65e75a20d 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -26,3 +26,6 @@ val lowercase_first_char : string -> string (** For extraction, turn a unicode string into an ascii-only one *) val is_basic_ascii : string -> bool val ascii_of_ident : string -> string + +(** Validate an UTF-8 string *) +val is_utf8 : string -> bool -- cgit v1.2.3 From 7461aaedef508570fba6334e18fd10d5b32bda0e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Mar 2016 21:35:42 +0100 Subject: Adding a test for the behaviour of open_constr described in #3777. --- test-suite/typeclasses/open_constr.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test-suite/typeclasses/open_constr.v diff --git a/test-suite/typeclasses/open_constr.v b/test-suite/typeclasses/open_constr.v new file mode 100644 index 000000000..5f1785c70 --- /dev/null +++ b/test-suite/typeclasses/open_constr.v @@ -0,0 +1,12 @@ +Tactic Notation "opose" open_constr(foo) := pose foo. +Class Foo := Build_Foo : Set. +Axiom f : forall `{Foo}, Set. +Set Printing Implicit. +Goal forall `{Foo}, True. +Proof. + intro H. + pose f. + opose f. + Fail let x := (eval hnf in P) in has_evar x. + let x := (eval hnf in P0) in has_evar x. + -- cgit v1.2.3 From 78b5670a0a1cf7ba31acabe710b311bf13df8745 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 3 Mar 2016 20:34:35 -0500 Subject: Fix a typo in dev/doc/changes.txt CQQ -> COQ --- dev/doc/changes.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9af..f7621a407 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,5 @@ ========================================= -= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = += CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= ** Refactoring : more mli interfaces and simpler grammar.cma ** -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- checker/check.mllib | 2 +- dev/printers.mllib | 2 +- kernel/csymtable.ml | 6 +- kernel/entries.mli | 2 +- kernel/pre_env.ml | 8 +-- kernel/pre_env.mli | 2 +- kernel/safe_typing.ml | 4 +- kernel/term_typing.ml | 4 +- lib/cEphemeron.ml | 89 +++++++++++++++++++++++++++ lib/cEphemeron.mli | 52 ++++++++++++++++ lib/ephemeron.ml | 89 --------------------------- lib/ephemeron.mli | 52 ---------------- lib/future.ml | 8 +-- lib/lib.mllib | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- proofs/proof_global.ml | 28 ++++----- stm/asyncTaskQueue.ml | 2 +- toplevel/obligations.ml | 16 ++--- 20 files changed, 187 insertions(+), 187 deletions(-) create mode 100644 lib/cEphemeron.ml create mode 100644 lib/cEphemeron.mli delete mode 100644 lib/ephemeron.ml delete mode 100644 lib/ephemeron.mli diff --git a/checker/check.mllib b/checker/check.mllib index 0d36e3a0f..902ab9ddf 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -32,7 +32,7 @@ CStack Util Ppstyle Errors -Ephemeron +CEphemeron Future CUnix System diff --git a/dev/printers.mllib b/dev/printers.mllib index ab7e9fc34..ad9a5d75e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -48,7 +48,7 @@ Rtree Heap Genarg Stateid -Ephemeron +CEphemeron Future RemoteCounter Monad diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index fc7e1b937..7e1a5d5b7 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -131,8 +131,8 @@ let key rk = match !rk with | None -> raise NotEvaluated | Some k -> - try Ephemeron.get k - with Ephemeron.InvalidKey -> raise NotEvaluated + try CEphemeron.get k + with CEphemeron.InvalidKey -> raise NotEvaluated (************************) (* traduction des patch *) @@ -171,7 +171,7 @@ let rec slot_for_getglobal env kn = | BCconstant -> set_global (val_of_constant kn) in (*Pp.msgnl(str"value stored at: "++int pos);*) - rk := Some (Ephemeron.create pos); + rk := Some (CEphemeron.create pos); pos and slot_for_fv env fv = diff --git a/kernel/entries.mli b/kernel/entries.mli index b2a77dd95..f94068f31 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -104,7 +104,7 @@ type side_eff = | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string type side_effect = { - from_env : Declarations.structure_body Ephemeron.key; + from_env : Declarations.structure_body CEphemeron.key; eff : side_eff; } diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index e1fe02595..df3495569 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -25,7 +25,7 @@ open Declarations (* The key attached to each constant is used by the VM to retrieve previous *) (* evaluations of the constant. It is essentially an index in the symbols table *) (* used by the VM. *) -type key = int Ephemeron.key option ref +type key = int CEphemeron.key option ref (** Linking information for the native compiler. *) @@ -50,17 +50,17 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) Ephemeron.key + | VKvalue of (values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref let force_lazy_val vk = match !vk with | VKnone -> None -| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key) +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_vals = (Id.t * lazy_val) list diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 23f9a3f41..99d3e2e25 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -19,7 +19,7 @@ type link_info = | LinkedInteractive of string | NotLinked -type key = int Ephemeron.key option ref +type key = int CEphemeron.key option ref type constant_key = constant_body * (link_info ref * key) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4c3264861..0926d35f6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -231,11 +231,11 @@ let constant_entry_of_private_constant = function let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } let private_con_of_scheme ~kind env cl = - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEscheme( List.map (fun (i,c) -> let cbo = Environ.lookup_constant c env.env in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 510f43542..fdbd1e3b1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -126,14 +126,14 @@ let check_signatures curmb sl = | None -> None, None | Some curmb -> try - let mb = Ephemeron.get mb in + let mb = CEphemeron.get mb in match sl with | None -> sl, None | Some n -> if List.length mb >= how_many && CList.skipn how_many mb == curmb then Some (n + how_many), Some mb else None, None - with Ephemeron.InvalidKey -> None, None in + with CEphemeron.InvalidKey -> None, None in let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in sl diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml new file mode 100644 index 000000000..a38ea11e1 --- /dev/null +++ b/lib/cEphemeron.ml @@ -0,0 +1,89 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* boxed_key = + (* TODO: take a random value here. Is there a random function in OCaml? *) + let bid = ref 0 in + (* According to OCaml Gc module documentation, Pervasives.ref is one of the + few ways of getting a boxed value the compiler will never alias. *) + fun () -> incr bid; Pervasives.ref (Pervasives.ref !bid) + +(* A phantom type to preserve type safety *) +type 'a key = boxed_key + +(* Comparing keys with == grants that if a key is unmarshalled (in the same + process where it was created or in another one) it is not mistaken for + an already existing one (unmarshal has no right to alias). If the initial + value of bid is taken at random, then one also avoids potential collisions *) +module HT = Hashtbl.Make(struct + type t = key_type ref + let equal k1 k2 = k1 == k2 + let hash id = !id +end) + +(* A key is the (unique) value inside a boxed key, hence it does not + keep its corresponding boxed key reachable (replacing key_type by boxed_key + would make the key always reachable) *) +let values : Obj.t HT.t = HT.create 1001 + +(* To avoid a race contidion between the finalization function and + get/create on the values hashtable, the finalization function just + enqueues in an imperative list the item to be collected. Being the list + imperative, even if the Gc enqueue an item while run_collection is operating, + the tail of the list is eventually set to Empty on completion. + Kudos to the authors of Why3 that came up with this solution for their + implementation of weak hash tables! *) +type imperative_list = cell ref +and cell = Empty | Item of key_type ref * imperative_list + +let collection_queue : imperative_list ref = ref (ref Empty) + +let enqueue x = collection_queue := ref (Item (!x, !collection_queue)) + +let run_collection () = + let rec aux l = match !l with + | Empty -> () + | Item (k, tl) -> HT.remove values k; aux tl in + let l = !collection_queue in + aux l; + l := Empty + +(* The only reference to the boxed key is the one returned, when the user drops + it the value eventually disappears from the values table above *) +let create (v : 'a) : 'a key = + run_collection (); + let k = mk_key () in + HT.add values !k (Obj.repr v); + Gc.finalise enqueue k; + k + +(* Avoid raising Not_found *) +exception InvalidKey +let get (k : 'a key) : 'a = + run_collection (); + try Obj.obj (HT.find values !k) + with Not_found -> raise InvalidKey + +(* Simple utils *) +let default k v = + try get k + with InvalidKey -> v + +let iter_opt k f = + match + try Some (get k) + with InvalidKey -> None + with + | None -> () + | Some v -> f v + +let clear () = run_collection () diff --git a/lib/cEphemeron.mli b/lib/cEphemeron.mli new file mode 100644 index 000000000..1200e4e20 --- /dev/null +++ b/lib/cEphemeron.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a key + +(* May raise InvalidKey *) +exception InvalidKey +val get : 'a key -> 'a + +(* These never fail. *) +val iter_opt : 'a key -> ('a -> unit) -> unit +val default : 'a key -> 'a -> 'a + +val clear : unit -> unit diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml deleted file mode 100644 index a38ea11e1..000000000 --- a/lib/ephemeron.ml +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* boxed_key = - (* TODO: take a random value here. Is there a random function in OCaml? *) - let bid = ref 0 in - (* According to OCaml Gc module documentation, Pervasives.ref is one of the - few ways of getting a boxed value the compiler will never alias. *) - fun () -> incr bid; Pervasives.ref (Pervasives.ref !bid) - -(* A phantom type to preserve type safety *) -type 'a key = boxed_key - -(* Comparing keys with == grants that if a key is unmarshalled (in the same - process where it was created or in another one) it is not mistaken for - an already existing one (unmarshal has no right to alias). If the initial - value of bid is taken at random, then one also avoids potential collisions *) -module HT = Hashtbl.Make(struct - type t = key_type ref - let equal k1 k2 = k1 == k2 - let hash id = !id -end) - -(* A key is the (unique) value inside a boxed key, hence it does not - keep its corresponding boxed key reachable (replacing key_type by boxed_key - would make the key always reachable) *) -let values : Obj.t HT.t = HT.create 1001 - -(* To avoid a race contidion between the finalization function and - get/create on the values hashtable, the finalization function just - enqueues in an imperative list the item to be collected. Being the list - imperative, even if the Gc enqueue an item while run_collection is operating, - the tail of the list is eventually set to Empty on completion. - Kudos to the authors of Why3 that came up with this solution for their - implementation of weak hash tables! *) -type imperative_list = cell ref -and cell = Empty | Item of key_type ref * imperative_list - -let collection_queue : imperative_list ref = ref (ref Empty) - -let enqueue x = collection_queue := ref (Item (!x, !collection_queue)) - -let run_collection () = - let rec aux l = match !l with - | Empty -> () - | Item (k, tl) -> HT.remove values k; aux tl in - let l = !collection_queue in - aux l; - l := Empty - -(* The only reference to the boxed key is the one returned, when the user drops - it the value eventually disappears from the values table above *) -let create (v : 'a) : 'a key = - run_collection (); - let k = mk_key () in - HT.add values !k (Obj.repr v); - Gc.finalise enqueue k; - k - -(* Avoid raising Not_found *) -exception InvalidKey -let get (k : 'a key) : 'a = - run_collection (); - try Obj.obj (HT.find values !k) - with Not_found -> raise InvalidKey - -(* Simple utils *) -let default k v = - try get k - with InvalidKey -> v - -let iter_opt k f = - match - try Some (get k) - with InvalidKey -> None - with - | None -> () - | Some v -> f v - -let clear () = run_collection () diff --git a/lib/ephemeron.mli b/lib/ephemeron.mli deleted file mode 100644 index 1200e4e20..000000000 --- a/lib/ephemeron.mli +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a key - -(* May raise InvalidKey *) -exception InvalidKey -val get : 'a key -> 'a - -(* These never fail. *) -val iter_opt : 'a key -> ('a -> unit) -> unit -val default : 'a key -> 'a -> 'a - -val clear : unit -> unit diff --git a/lib/future.ml b/lib/future.ml index 5cd2beba9..e8f33db5e 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -62,7 +62,7 @@ and 'a comp = | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = - | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key + | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key | Finished of 'a and 'a computation = 'a comput ref @@ -70,13 +70,13 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x))) + ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) | Ongoing (name, x) -> - try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c - with Ephemeron.InvalidKey -> + try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c + with CEphemeron.InvalidKey -> name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null)) type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] diff --git a/lib/lib.mllib b/lib/lib.mllib index f3f6ad8fc..6805ce491 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,6 +15,6 @@ Rtree Heap Unionfind Genarg -Ephemeron +CEphemeron Future RemoteCounter diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda..18200307a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true, Ephemeron.create hook + get_proof_clean true, CEphemeron.create hook end diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index aa47e2619..2449678a1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 23f1da1ba..e5c756f56 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook Ephemeron.key -> unit + unit Lemmas.declaration_hook CEphemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f22cdbcc8..541f299d4 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,7 +36,7 @@ let find_proof_mode n = Errors.error (Format.sprintf "No proof mode named \"%s\"." n) let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (Ephemeron.create m) + Hashtbl.add proof_modes n (CEphemeron.create m) (* initial mode: standard mode *) let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } @@ -52,7 +52,7 @@ let _ = optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; optread = begin fun () -> - (Ephemeron.default !default_proof_mode standard).name + (CEphemeron.default !default_proof_mode standard).name end; optwrite = begin fun n -> default_proof_mode := find_proof_mode n @@ -83,12 +83,12 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; - terminator : proof_terminator Ephemeron.key; + terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - mode : proof_mode Ephemeron.key; + mode : proof_mode CEphemeron.key; universe_binders: universe_binders option; } @@ -103,11 +103,11 @@ let current_proof_mode = ref !default_proof_mode let update_proof_mode () = match !pstates with | { mode = m } :: _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := m; - Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) | _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := find_proof_mode "No" (* combinators for the current_proof lists *) @@ -215,9 +215,9 @@ let set_proof_mode mn = set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) let activate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) let disactivate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) (** [start_proof sigma id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and @@ -230,7 +230,7 @@ let disactivate_proof_mode mode = let start_proof sigma id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.start sigma goals; endline_tactic = None; section_vars = None; @@ -242,7 +242,7 @@ let start_proof sigma id ?pl str goals terminator = let start_dependent_proof id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.dependent_start goals; endline_tactic = None; section_vars = None; @@ -375,7 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, - fun pr_ending -> Ephemeron.get terminator pr_ending + fun pr_ending -> CEphemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -423,11 +423,11 @@ let close_proof ~keep_body_ucst_separate fix_exn = (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator let set_terminator hook = match !pstates with | [] -> raise NoCurrentProof - | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps + | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cc9732604..5f018ec39 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -314,7 +314,7 @@ module Make(T : Task) = struct let response = slave_respond request in report_status "Idle"; marshal_response (Option.get !slave_oc) response; - Ephemeron.clear () + CEphemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 7e0d30a63..615257a1c 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -324,11 +324,11 @@ type program_info_aux = { prg_sign: named_context_val; } -type program_info = program_info_aux Ephemeron.key +type program_info = program_info_aux CEphemeron.key let get_info x = - try Ephemeron.get x - with Ephemeron.InvalidKey -> + try CEphemeron.get x + with CEphemeron.InvalidKey -> Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker") let assumption_message = Declare.assumption_message @@ -461,7 +461,7 @@ let subst_deps_obl obls obl = module ProgMap = Map.Make(Id) -let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m) +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] @@ -682,7 +682,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m; + if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; !i exception Found of program_info @@ -690,7 +690,7 @@ exception Found of program_info let map_first m = try ProgMap.iter (fun _ v -> - if snd (Ephemeron.get v).prg_obligations > 0 then + if snd (CEphemeron.get v).prg_obligations > 0 then raise (Found v)) m; assert(false) with Found x -> x @@ -1016,7 +1016,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit else ( let len = Array.length obls in let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n (Ephemeron.create prg); + progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res @@ -1030,7 +1030,7 @@ let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(r (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook - in progmap_add n (Ephemeron.create prg)) l; + in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished -- cgit v1.2.3 From 120053a50f87bd53398eedc887fa5e979f56f112 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 18:17:56 +0100 Subject: This fix is probably not enough to justify that there are no problems with primitive projections and prop. ext. or univalence, but at least it prevents known proofs of false (see discussion on #4588). --- kernel/inductive.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 80dc69042..fbe0920bc 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -814,7 +814,15 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> Subterm (Strict, wf) + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + Subterm (Strict, List.nth wf_args n) | Dead_code -> Dead_code | Not_subterm -> Not_subterm) -- cgit v1.2.3 From 35cc038e96395b0f4eaaeed3a5a48e6da2293f7e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 19:01:35 +0100 Subject: Fix #4607: do not read native code files if native compiler was disabled. --- library/library.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/library.ml b/library/library.ml index 79e5792c0..ccda57c2c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -171,9 +171,8 @@ 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 - (* This will not produce errors or warnings if the native compiler was - not enabled *) - Nativelib.link_library ~prefix ~dirname ~basename:f + if not Coq_config.no_native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] -- cgit v1.2.3 From 32baedf7a3aebb96f7dd2c7d90a1aef40ed93792 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Mar 2016 18:16:31 +0100 Subject: Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)". The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation. --- grammar/argextend.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 8def9537c..cb0f7d2d3 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -120,7 +120,7 @@ let make_possibly_empty_subentries loc s cl = let make_act loc act pil = let rec make = function - | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< Pcoq.Gram.action (fun loc -> let loc = Compat.to_coqloc loc in ($act$ : 'a)) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.Id.to_string p in <:expr< -- cgit v1.2.3