From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:06:32 +0100 Subject: Remove Refine Instance Mode option --- .../07-commands-and-options/09530-rm-unknown.rst | 6 ++++++ doc/sphinx/addendum/type-classes.rst | 15 +-------------- doc/sphinx/changes.rst | 7 +++---- plugins/ltac/rewrite.ml | 2 +- test-suite/success/Typeclasses.v | 4 +--- theories/Compat/Coq89.v | 1 - vernac/classes.ml | 18 ++++-------------- vernac/classes.mli | 1 - 8 files changed, 16 insertions(+), 38 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/09530-rm-unknown.rst diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst new file mode 100644 index 0000000000..78874cadb1 --- /dev/null +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -0,0 +1,6 @@ +- Deprecated flag `Refine Instance Mode` has been removed. + (`#09530 `_, fixes + `#3632 `_, `#3890 + `_ and `#4638 + `_ + by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ee417f269d..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -316,7 +316,7 @@ Summary of the commands This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and fields defined by :token:`field_def`, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An @@ -563,19 +563,6 @@ Settings of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this option to 0 turns that option off. -.. flag:: Refine Instance Mode - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5e337bcef0..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -486,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 `_, and `#9825 `_, diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a68efa4713..963b7189f9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3888cafed3..736d05fefc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,9 +198,7 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. - Set Refine Instance Mode. - Instance eqa : Eq nat := _. constructor. Qed. - Unset Refine Instance Mode. + Instance eqa : Eq nat. Qed. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 05d63d9a47..49e0af9b2c 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,4 +14,3 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. -Set Refine Instance Mode. diff --git a/vernac/classes.ml b/vernac/classes.ml index ece9fc8937..05a75ab435 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration open Decl_kinds open Entries -let refine_instance = ref false - -let () = Goptions.(declare_bool_option { - optdepr = true; - optname = "definition of instances by refining"; - optkey = ["Refine";"Instance";"Mode"]; - optread = (fun () -> !refine_instance); - optwrite = (fun b -> refine_instance := b) -}) - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -419,7 +409,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po | None -> pstate) ()) -let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -503,7 +493,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program let term = to_constr sigma (Option.get term) in (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) - else if program_mode || refine || Option.is_empty props then + else if program_mode || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate @@ -550,7 +540,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode +let new_instance ~pstate ?(global=false) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -566,7 +556,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = diff --git a/vernac/classes.mli b/vernac/classes.mli index e7f90ff306..57bb9ce312 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -48,7 +48,6 @@ val declare_instance_constant : val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> - ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> -- cgit v1.2.3 From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:48:36 +0100 Subject: Remove VtUnknown classification This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. --- plugins/ltac/g_rewrite.mlg | 2 +- stm/stm.ml | 51 +-------------------------------------- stm/vernac_classifier.ml | 36 +++++++++++++++------------ test-suite/bugs/closed/bug_3890.v | 12 +++++++++ test-suite/bugs/closed/bug_4580.v | 1 - test-suite/bugs/closed/bug_4638.v | 12 +++++++++ test-suite/bugs/opened/bug_3890.v | 22 ----------------- vernac/vernacextend.ml | 1 - vernac/vernacextend.mli | 1 - 9 files changed, 47 insertions(+), 91 deletions(-) create mode 100644 test-suite/bugs/closed/bug_3890.v create mode 100644 test-suite/bugs/closed/bug_4638.v delete mode 100644 test-suite/bugs/opened/bug_3890.v diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 469551809c..12b12bc7b0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { VtUnknown, VtNow } + => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { add_morphism_infer atts m n } diff --git a/stm/stm.ml b/stm/stm.ml index 21618bc044..6f7cefb582 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -364,7 +364,6 @@ module VCS : sig val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option - val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -572,6 +571,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i + | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -611,7 +611,6 @@ end = struct (* {{{ *) info.state <- new_state let get_proof_mode id = (get_info id).proof_mode - let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in @@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id parsing_state) new_ids; `Ok - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - if not (get_allow_nested_proofs ()) && in_proof then - "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." - |> Pp.str - |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy newtip - |> Exninfo.iraise - else - let id = VCS.new_node ~id:newtip proof_mode () in - let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - (* Vernac x may or may not start a proof *) - if not in_proof && PG_compat.there_are_pending_proofs () then - begin - let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = function - (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (_,_ , None, _) -> GuaranteesOpacity - | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); - VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); - end else begin - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Proof _ -> - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); - end; - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~doc ~safe_id:head_id ~cache:true step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow.") - | VtProofMode pm, VtNow -> let proof_mode = Pvernac.lookup_proof_mode pm in let id = VCS.new_node ~id:newtip proof_mode () in @@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtProofMode _, VtLater -> anomaly(str"classifier: VtProofMode must imply VtNow.") - end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4a4c5c94e9..7cecd801e4 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,7 +21,6 @@ let string_of_parallel = function | `No -> "" let string_of_vernac_type = function - | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" @@ -61,7 +60,7 @@ let options_affecting_stm_scheduling = ] let classify_vernac e = - let static_classifier ~poly e = match e with + let static_classifier ~atts e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) @@ -97,15 +96,18 @@ let classify_vernac e = VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -115,8 +117,9 @@ let classify_vernac e = then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -185,8 +188,12 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow + | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater + | VernacInstance (_,((name,_),_,_),_,_) -> + VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ @@ -201,9 +208,8 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (f, e) -> - let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly e + | VernacExpr (atts, e) -> + static_classifier ~atts e | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,e) | VernacRedirect (_, e) -> static_control_classifier e @@ -214,6 +220,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)) + | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater)) in static_control_classifier e diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v new file mode 100644 index 0000000000..e1823ac54c --- /dev/null +++ b/test-suite/bugs/closed/bug_3890.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo. + +Instance bar : Bar. +exact Type. +Defined. + +Defined. diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v index a8a446cc9b..3f40569d61 100644 --- a/test-suite/bugs/closed/bug_4580.v +++ b/test-suite/bugs/closed/bug_4580.v @@ -2,6 +2,5 @@ Require Import Program. Class Foo (A : Type) := foo : A. -Unset Refine Instance Mode. Program Instance f1 : Foo nat := S _. Next Obligation. exact 0. Defined. diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v new file mode 100644 index 0000000000..951fe5302b --- /dev/null +++ b/test-suite/bugs/closed/bug_4638.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. + +Goal True. + +Instance foo: Foo. +Qed. + +trivial. + +Qed. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ef06e59316..730f5fd6da 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -36,7 +36,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d89eaffd9..54e08d0e95 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -52,7 +52,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = -- cgit v1.2.3