diff options
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 | ||||
-rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 13 | ||||
-rw-r--r-- | stm/stm.ml | 26 | ||||
-rw-r--r-- | stm/vernac_classifier.ml | 9 | ||||
-rw-r--r-- | stm/vernac_classifier.mli | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/2969.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3377.v | 3 | ||||
-rw-r--r-- | test-suite/bugs/closed/4069.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4198.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4782.v | 2 | ||||
-rw-r--r-- | test-suite/ide/undo012.fake | 1 | ||||
-rw-r--r-- | test-suite/ide/undo013.fake | 1 | ||||
-rw-r--r-- | test-suite/ide/undo014.fake | 1 | ||||
-rw-r--r-- | test-suite/ide/undo015.fake | 1 | ||||
-rw-r--r-- | test-suite/ide/undo016.fake | 1 | ||||
-rw-r--r-- | test-suite/output/Cases.v | 1 | ||||
-rw-r--r-- | test-suite/output/ltac.v | 3 | ||||
-rw-r--r-- | test-suite/success/Inversion.v | 2 | ||||
-rw-r--r-- | test-suite/success/RecTutorial.v | 2 | ||||
-rw-r--r-- | test-suite/success/destruct.v | 1 | ||||
-rw-r--r-- | test-suite/success/refine.v | 4 | ||||
-rw-r--r-- | test-suite/success/sideff.v | 2 |
23 files changed, 74 insertions, 12 deletions
@@ -18,6 +18,9 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +- Nested proofs may be enabled through the option `Nested Proofs Allowed`. + By default, they are disabled and produce an error. The deprecation + warning which used to occur when using nested proofs has been removed. Tactics diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 4dcd7deb1..d17043105 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1339,7 +1339,8 @@ using the keyword :cmd:`Qed`. .. note:: - #. Several statements can be simultaneously asserted. + #. Several statements can be simultaneously asserted provided option + :opt:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6d0b27728..eba0db3ff 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -113,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). + .. seealso:: :opt:`Nested Proofs Allowed` + .. cmdv:: Abort All Aborts all current goals. @@ -561,6 +563,17 @@ Controlling the effect of proof editing commands has to be used to move the assumptions to the local context. +.. opt:: Nested Proofs Allowed + + When turned on (it is off by default), this option enables support for nested + proofs: a new assertion command can be inserted before the current proof is + finished, in which case Coq will temporarily switch to the proof of this + *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` + or :cmd:`Defined`), its statement will be made available (as if it had been + proved before starting the previous proof) and Coq will switch back to the + proof of the previous assertion. + + Controlling memory usage ------------------------ diff --git a/stm/stm.ml b/stm/stm.ml index 9ea6a305e..20409c25e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2113,12 +2113,6 @@ let delegate name = || VCS.is_vio_doc () || !cur_opt.async_proofs_full -let warn_deprecated_nested_proofs = - CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" - (fun () -> - strbrk ("Nested proofs are deprecated and will "^ - "stop working in a future Coq version")) - let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -2200,8 +2194,7 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, accn, name, delegate name) - | `Sideff _ -> - warn_deprecated_nested_proofs (); + | `Sideff (CherryPickEnv,_) -> `Sync (no_name,`NestedProof) | _ -> `Sync (no_name,`Unknown) in let make_sync why = function @@ -2771,6 +2764,14 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok +let allow_nested_proofs = ref false +let _ = Goptions.declare_bool_option + { Goptions.optdepr = false; + Goptions.optname = "Nested Proofs Allowed"; + Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; + Goptions.optread = (fun () -> !allow_nested_proofs); + Goptions.optwrite = (fun b -> allow_nested_proofs := b) } + let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); @@ -2802,6 +2803,15 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> + + if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c08cc6e36..e01dcbcb6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -54,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list = | Names.Anonymous -> [] | Names.Name n -> [n] +let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] + +let options_affecting_stm_scheduling = + [ Vernacentries.universe_polymorphism_option_name; + stm_allow_nested_proofs_option_name ] + let classify_vernac e = let static_classifier ~poly 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. *) | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) - when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + when CList.exists (CList.equal String.equal l) + options_affecting_stm_scheduling -> VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index abbc04e89..45fbfb42a 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -25,3 +25,4 @@ val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification val classify_as_proofstep : vernac_classification +val stm_allow_nested_proofs_option_name : string list diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v index a03adbd73..7b1a26178 100644 --- a/test-suite/bugs/closed/2969.v +++ b/test-suite/bugs/closed/2969.v @@ -12,6 +12,7 @@ eexists. reflexivity. Grab Existential Variables. admit. +Admitted. (* Alternative variant which failed but without raising anomaly *) @@ -24,3 +25,4 @@ clearbody n n0. exact I. Grab Existential Variables. admit. +Admitted. diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v index 8e9e3933c..abfcf1d35 100644 --- a/test-suite/bugs/closed/3377.v +++ b/test-suite/bugs/closed/3377.v @@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}. Goal fst (@pair Type Type Type Type). Set Printing All. match goal with |- ?f ?x => set (foo := f x) end. +Abort. Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x). Proof. @@ -12,6 +13,6 @@ Proof. lazymatch goal with | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f end. - (* Toplevel input, characters 7-44: Error: No matching clauses for match. *) +Abort. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 606c6e084..668f6bb42 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -41,6 +41,8 @@ Proof. f_equal. 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l and skipn n l = l *) +Abort. + Require Import List. Fixpoint replicate {A} (n : nat) (x : A) : list A := match n with 0 => nil | S n => x :: replicate n x end. diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index eb37141bc..28800ac05 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), match goal with | [ |- context G[@hd] ] => idtac end. +Abort. (* This second example comes from CFGV where inspecting subterms of a match is expecting to inspect first the term to match (even though @@ -35,3 +36,4 @@ Ltac mydestruct := Goal forall x, match x with 0 => 0 | _ => 0 end = 0. intros. mydestruct. +Abort. diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index dbd71035d..1e1a4cb9c 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +Abort. (* A simplification of an example from coquelicot, which was failing at some time after a fix #4782 was committed. *) @@ -21,4 +22,5 @@ Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. intros. apply (F _ _) with (x,x). +Abort. diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake index b3d1c6d53..c95df1b11 100644 --- a/test-suite/ide/undo012.fake +++ b/test-suite/ide/undo012.fake @@ -3,6 +3,7 @@ # # Test backtracking in presence of nested proofs # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index 921a9d0f0..a3ccefd2c 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Second, trigger the undo of an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index f5fe77470..13e718229 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Third, undo inside an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index a1e5c947b..9cbd64460 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fourth, undo from an inner proof to a above proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index f9414c1ea..15bd3cc92 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fifth, undo from an inner proof to a previous inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index caf3b2870..4740c009a 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -163,6 +163,7 @@ match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. Show. +Abort. Lemma lem5 (p:nat) : eq_refl p = eq_refl p. let y := fresh "n" in (* Checking that y is hidden *) diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 6adbe95dd..901b1e3aa 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -37,17 +37,20 @@ Fail g1 I. Fail f1 I. Fail g2 I. Fail f2 I. +Abort. Ltac h x := injection x. Goal True -> False. Fail h I. intro H. Fail h H. +Abort. (* Check printing of the "var" argument "Hx" *) Ltac m H := idtac H; exact H. Goal True. let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. +Abort. (* Check consistency of interpretation scopes (#4398) *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ca8da3948..ee540d710 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1. intros. eapply trans_eq. inversion H. +Abort. (* Check that the part of "injection" that is called by "inversion" does the same number of intros as the number of equations @@ -136,6 +137,7 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. +Abort. (* Was failing at some time between 7 and 10 September 2014 *) (* even though, it is not clear that the resulting context is interesting *) diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 29350d620..6370cab6b 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -589,6 +589,8 @@ Close Scope Z_scope. Theorem S_is_not_O : forall n, S n <> 0. +Set Nested Proofs Allowed. + Definition Is_zero (x:nat):= match x with | 0 => True | _ => False diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 6fbe61a9b..d1d384659 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -422,6 +422,7 @@ Abort. Goal forall b:bool, b = b. intros. destruct b eqn:H. +Abort. (* Check natural instantiation behavior when the goal has already an evar *) diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 22fb4d757..40986e57c 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -121,14 +121,16 @@ Abort. (* Wish 1988: that fun forces unfold in refine *) Goal (forall A : Prop, A -> ~~A). -Proof. refine(fun A a f => _). +Proof. refine(fun A a f => _). Abort. (* Checking beta-iota normalization of hypotheses in created evars *) Goal {x|x=0} -> True. refine (fun y => let (x,a) := y in _). match goal with a:_=0 |- _ => idtac end. +Abort. Goal (forall P, {P 0}+{P 1}) -> True. refine (fun H => if H (fun x => x=x) then _ else _). match goal with _:0=0 |- _ => idtac end. +Abort. diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v index 3c0b81568..b9a1273b1 100644 --- a/test-suite/success/sideff.v +++ b/test-suite/success/sideff.v @@ -5,6 +5,8 @@ Proof. apply (const tt tt). Qed. +Set Nested Proofs Allowed. + Lemma foobar' : unit. Lemma aux : forall A : Type, A -> unit. Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed. |