From 9eded874620c40bcc103eaebb6070cdb230eecfb Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 28 Oct 2024 14:27:14 -0700 Subject: [PATCH] fix: remove `withoutRecover` from `apply` elaboration (#5862) The assumptions behind disabling error recovery for the `apply` tactic no longer seem to hold, since tactic combinators like `first` themselves disable error recovery when it makes sense. This addresses part of #3831 Breaking change: `elabTermForApply` no longer uses `withoutRecover`. Tactics using `elabTermForApply` should evaluate whether it makes sense to wrap it with `withoutRecover`, which is generally speaking when it's used to elaborate identifiers. --- src/Lean/Elab/Tactic/Conv/Unfold.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 40 ++------------------------- src/Lean/Elab/Tactic/Unfold.lean | 2 +- tests/lean/1719.lean.expected.out | 4 --- tests/lean/run/1037.lean | 7 +++++ 5 files changed, 12 insertions(+), 43 deletions(-) diff --git a/src/Lean/Elab/Tactic/Conv/Unfold.lean b/src/Lean/Elab/Tactic/Conv/Unfold.lean index 2bbc9439c2db..f8679286760c 100644 --- a/src/Lean/Elab/Tactic/Conv/Unfold.lean +++ b/src/Lean/Elab/Tactic/Conv/Unfold.lean @@ -13,7 +13,7 @@ open Meta @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do for declNameId in stx[1].getArgs do withRef declNameId do - let e ← elabTermForApply declNameId (mayPostpone := false) + let e ← withoutRecover <| elabTermForApply declNameId (mayPostpone := false) match e with | .const declName _ => applySimpResult (← unfold (← getLhs) declName) diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index e7a7e382a841..1d05fc3e9577 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -257,45 +257,11 @@ def elabTermForApply (stx : Syntax) (mayPostpone := true) : TacticM Expr := do match (← Term.resolveId? stx (withInfo := true)) with | some e => return e | _ => pure () - /- - By disabling the "error recovery" (and consequently "error to sorry") feature, - we make sure an `apply e` fails without logging an error message. - The motivation is that `apply` is frequently used when writing tactic such as - ``` - cases h <;> intro h' <;> first | apply t[h'] | .... - ``` - Here the type of `h'` may be different in each case, and the term `t[h']` containing `h'` may even fail to - be elaborated in some cases. When this happens we want the tactic to fail without reporting any error to the user, - and the next tactic is tried. - - A drawback of disabling "error to sorry" is that there is no error recovery after the error is thrown, and features such - as auto-completion are affected. - - By disabling "error to sorry", we also limit ourselves to at most one error at `t[h']`. - - By disabling "error to sorry", we also miss the opportunity to catch mistakes in tactic code such as - `first | apply nonsensical-term | assumption` - - This should not be a big problem for the `apply` tactic since we usually provide small terms there. - - Note that we do not disable "error to sorry" at `exact` and `refine` since they are often used to elaborate big terms, - and we do want error recovery there, and we want to see the error messages. - - We should probably provide options for allowing users to control this behavior. - - see issue #1037 - - More complex solution: - - We do not disable "error to sorry" - - We elaborate term and check whether errors were produced - - If there are other tactic branches and there are errors, we remove the errors from the log, and throw a new error to force the tactic to backtrack. - -/ - withoutRecover <| elabTerm stx none mayPostpone + elabTerm stx none mayPostpone -def getFVarId (id : Syntax) : TacticM FVarId := withRef id do +def getFVarId (id : Syntax) : TacticM FVarId := withRef id <| withMainContext do -- use apply-like elaboration to suppress insertion of implicit arguments - let e ← withMainContext do - elabTermForApply id (mayPostpone := false) + let e ← withoutRecover <| elabTermForApply id (mayPostpone := false) match e with | Expr.fvar fvarId => return fvarId | _ => throwError "unexpected term '{e}'; expected single reference to variable" diff --git a/src/Lean/Elab/Tactic/Unfold.lean b/src/Lean/Elab/Tactic/Unfold.lean index 0bae5e82b89e..d62c6e8b21bd 100644 --- a/src/Lean/Elab/Tactic/Unfold.lean +++ b/src/Lean/Elab/Tactic/Unfold.lean @@ -30,7 +30,7 @@ def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do go declNameId loc where go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId do - let e ← elabTermForApply declNameId (mayPostpone := false) + let e ← withoutRecover <| elabTermForApply declNameId (mayPostpone := false) match e with | .const declName _ => withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'") diff --git a/tests/lean/1719.lean.expected.out b/tests/lean/1719.lean.expected.out index 15d27d9932b3..fc7b8a40c51c 100644 --- a/tests/lean/1719.lean.expected.out +++ b/tests/lean/1719.lean.expected.out @@ -1,6 +1,2 @@ 1719.lean:2:8-2:12: error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant ?m -1719.lean:1:27-2:12: error: unsolved goals -P Q : Prop -h : P -⊢ P ∨ Q diff --git a/tests/lean/run/1037.lean b/tests/lean/run/1037.lean index df87681beb31..b876edbab3ba 100644 --- a/tests/lean/run/1037.lean +++ b/tests/lean/run/1037.lean @@ -11,3 +11,10 @@ example (p q r s: Prop) (h1: p -> s) (h2: q -> s) (h3: r -> s) (try (apply h.elim <;> intro h)) <;> revert h <;> assumption; } + +/-! +Verify that `withoutRecover` is not necessary for `apply`. +This is because `first` enables it itself. +-/ +example (p : Prop) (h : p) : p := by + first | apply bogusTerm | assumption