From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- kernel/entries.mli | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) (limited to 'kernel/entries.mli') diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d355..e058519e96 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -54,11 +54,11 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects -type const_entry_body = proof_output Future.computation +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation -type definition_entry = { - const_entry_body : const_entry_body; +type 'a definition_entry = { + const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) @@ -78,8 +78,8 @@ type projection_entry = { proj_entry_ind : mutual_inductive; proj_entry_arg : int } -type constant_entry = - | DefinitionEntry of definition_entry +type 'a constant_entry = + | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -96,3 +96,16 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_eff = + | SEsubproof of constant * Declarations.constant_body * seff_env + | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + +type side_effect = { + from_env : Declarations.structure_body Ephemeron.key; + eff : side_eff; +} + +type side_effects = side_effect list -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/entries.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/entries.mli') diff --git a/kernel/entries.mli b/kernel/entries.mli index e058519e96..b2a77dd950 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- kernel/entries.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/entries.mli') diff --git a/kernel/entries.mli b/kernel/entries.mli index b2a77dd950..f94068f31e 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; } -- cgit v1.2.3