fix: unresolved holes in the exact tactic, backtracking issues

This commit also adds the `throwAbortTactic` for throwing "silent"
exceptions in `TacticM`.

src/Lean/Elab/Exception.lean

@@ -12,6 +12,7 @@ builtin_initialize postponeExceptionId : InternalExceptionId ← registerInterna
 builtin_initialize unsupportedSyntaxExceptionId : InternalExceptionId ← registerInternalExceptionId `unsupportedSyntax
 builtin_initialize abortCommandExceptionId : InternalExceptionId ← registerInternalExceptionId `abortCommandElab
 builtin_initialize abortTermExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTermElab
+builtin_initialize abortTacticExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTactic
 builtin_initialize autoBoundImplicitExceptionId : InternalExceptionId ← registerInternalExceptionId `autoBoundImplicit
 
 def throwPostpone [MonadExceptOf Exception m] : m α :=
@@ -46,8 +47,17 @@ def throwAbortCommand {α m} [MonadExcept Exception m] : m α :=
 def throwAbortTerm {α m} [MonadExcept Exception m] : m α :=
   throw <| Exception.internal abortTermExceptionId
 
+-- Throw exception to abort evaluation of the current tactic without producing any error message
+def throwAbortTactic {α m} [MonadExcept Exception m] : m α :=
+  throw <| Exception.internal abortTacticExceptionId
+
+def isAbortTacticException (ex : Exception) : Bool :=
+  match ex with
+  | Exception.internal id .. => id == abortTacticExceptionId
+  | _ => false
+
 def isAbortExceptionId (id : InternalExceptionId) : Bool :=
-  id == abortCommandExceptionId || id == abortTermExceptionId
+  id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId
 
 def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
   let pos := fileMap.toPosition pos

src/Lean/Elab/SyntheticMVars.lean

@@ -193,26 +193,14 @@ private def getSomeSynthethicMVarsRef : TermElabM Syntax := do
 
 mutual
 
-  partial def liftTacticElabM {α} (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
-    withMVarContext mvarId do
-      let savedSyntheticMVars := (← get).syntheticMVars
-      modify fun s => { s with syntheticMVars := [] }
-      try
-        let a ← x.run' { main := mvarId } { goals := [mvarId] }
-        synthesizeSyntheticMVars (mayPostpone := false)
-        pure a
-      finally
-        modify fun s => { s with syntheticMVars := savedSyntheticMVars }
-
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
     /- Recall, `tacticCode` is the whole `by ...` expression. -/
     let byTk := tacticCode[0]
     let code := tacticCode[1]
     modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
-    let remainingGoals ← withInfoHole mvarId <|
-      liftTacticElabM mvarId do
-        withTacticInfoContext tacticCode (evalTactic code)
-        getUnsolvedGoals
+    let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+       withTacticInfoContext tacticCode (evalTactic code)
+       synthesizeSyntheticMVars (mayPostpone := false)
     unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
 
   /-- Try to synthesize the given pending synthetic metavariable. -/

src/Lean/Elab/Tactic/Basic.lean

@@ -41,6 +41,47 @@ structure SavedState where
 abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
 abbrev Tactic  := Syntax → TacticM Unit
 
+def getGoals : TacticM (List MVarId) :=
+  return (← get).goals
+
+def setGoals (mvarIds : List MVarId) : TacticM Unit :=
+  modify fun s => { s with goals := mvarIds }
+
+def pruneSolvedGoals : TacticM Unit := do
+  let gs ← getGoals
+  let gs ← gs.filterM fun g => not <$> isExprMVarAssigned g
+  setGoals gs
+
+def getUnsolvedGoals : TacticM (List MVarId) := do
+  pruneSolvedGoals
+  getGoals
+
+@[inline] private def TacticM.runCore (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
+  x ctx |>.run s
+
+@[inline] private def TacticM.runCore' (x : TacticM α) (ctx : Context) (s : State) : TermElabM α :=
+  Prod.fst <$> x.runCore ctx s
+
+def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
+  withMVarContext mvarId do
+   let savedSyntheticMVars := (← get).syntheticMVars
+   modify fun s => { s with syntheticMVars := [] }
+   let aux : TacticM (List MVarId) :=
+     /- Important: the following `try` does not backtrack the state.
+        This is intentional because we don't want to backtrack the error messages when we catch the "abort internal exception"
+        We must define `run` here because we define `MonadExcept` instance for `TacticM` -/
+     try
+       x; getUnsolvedGoals
+     catch ex =>
+       if isAbortTacticException ex then
+         getUnsolvedGoals
+       else
+         throw ex
+   try
+     aux.runCore' { main := mvarId } { goals := [mvarId] }
+   finally
+     modify fun s => { s with syntheticMVars := savedSyntheticMVars }
+
 protected def saveState : TacticM SavedState :=
   return { term := (← Term.saveState), tactic := (← get) }
 
@@ -48,24 +89,6 @@ def SavedState.restore (b : SavedState) : TacticM Unit := do
   b.term.restore
   set b.tactic
 
-instance : MonadBacktrack SavedState TacticM where
-  saveState := Tactic.saveState
-  restoreState b := b.restore
-
-@[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
-  let b ← saveState
-  try x catch ex => b.restore; h ex
-
-instance : MonadExcept Exception TacticM where
-  throw    := throw
-  tryCatch := Tactic.tryCatch
-
-@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do
-  try x catch _ => y
-
-instance {α} : OrElse (TacticM α) where
-  orElse := Tactic.orElse
-
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Term.Context).currMacroScope
 protected def getMainModule     : TacticM Name       := do pure (← getEnv).mainModule
 
@@ -74,6 +97,13 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
 
 @[builtinInit mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic
 
+/-
+Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
+the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
+and this is bad when rethrowing the exception at the `catch` block in these methods.
+We marked these places with a `(*)` in these methods.
+-/
+
 private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tactic) : TacticM Unit := do
   let rec loop : List Tactic → TacticM Unit
     | []              => throwErrorAt stx "unexpected syntax {indentD stx}"
@@ -83,7 +113,7 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact
       catch
       | ex@(Exception.error _ _) =>
         match evalFns with
-        | []      => throw ex
+        | []      => throw ex -- (*)
         | evalFns => s.restore; loop evalFns
       | ex@(Exception.internal id _) =>
         if id == unsupportedSyntaxExceptionId then
@@ -92,9 +122,6 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact
           throw ex
   loop tactics
 
-def getGoals : TacticM (List MVarId) :=
-  return (← get).goals
-
 def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
   return Info.ofTacticInfo {
     mctxBefore    := mctxBefore
@@ -120,7 +147,7 @@ mutual
           let stx' ← adaptMacro m stx
           evalTactic stx'
         catch ex =>
-          if ms.isEmpty then throw ex
+          if ms.isEmpty then throw ex -- (*)
           loop ms
     loop macros
 
@@ -138,7 +165,7 @@ mutual
           stx.getArgs.forM evalTactic
         else do
           trace[Elab.step] "{stx}"
-          let s ← saveState
+          let s ← Tactic.saveState
           let table := (tacticElabAttribute.ext.getState (← getEnv)).table
           let k := stx.getKind
           match table.find? k with
@@ -151,6 +178,24 @@ mutual
 
 end
 
+instance : MonadBacktrack SavedState TacticM where
+  saveState := Tactic.saveState
+  restoreState b := b.restore
+
+@[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
+  let b ← saveState
+  try x catch ex => b.restore; h ex
+
+instance : MonadExcept Exception TacticM where
+  throw    := throw
+  tryCatch := Tactic.tryCatch
+
+@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do
+  try x catch _ => y
+
+instance {α} : OrElse (TacticM α) where
+  orElse := Tactic.orElse
+
 /-
   Save the current tactic state for a token `stx`.
   This method is a no-op if `stx` has no position information.
@@ -171,9 +216,6 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
   let stx' ← exp stx
   withMacroExpansion stx stx' $ evalTactic stx'
 
-def setGoals (mvarIds : List MVarId) : TacticM Unit :=
-  modify fun s => { s with goals := mvarIds }
-
 def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
@@ -184,15 +226,6 @@ def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (mvarId :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun s => { s with goals := mvarIds ++ mvarIds' }
 
-def pruneSolvedGoals : TacticM Unit := do
-  let gs ← getGoals
-  let gs ← gs.filterM fun g => not <$> isExprMVarAssigned g
-  setGoals gs
-
-def getUnsolvedGoals : TacticM (List MVarId) := do
-  pruneSolvedGoals
-  getGoals
-
 /-- Return the first goal. -/
 def getMainGoal : TacticM MVarId := do
   loop (← getGoals)
@@ -601,10 +634,4 @@ where
 
 builtin_initialize registerTraceClass `Elab.tactic
 
-@[inline] def TacticM.run (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
-  x ctx |>.run s
-
-@[inline] def TacticM.run' (x : TacticM α) (ctx : Context) (s : State) : TermElabM α :=
-  Prod.fst <$> x.run ctx s
-
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -33,14 +33,21 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
     return e
 
 /- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
-def closeMainGoalUsing (x : Expr → TacticM Expr) : TacticM Unit :=
+def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
   withMainContext do
-    closeMainGoal (← x (← getMainTarget))
+    closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
+
+private def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
+   if (← Term.logUnassignedUsingErrorInfos mvarIds) then
+     throwAbortTactic
 
 @[builtinTactic «exact»] def evalExact : Tactic := fun stx =>
   match stx with
-  | `(tactic| exact $e) => closeMainGoalUsing (fun type => elabTermEnsuringType e type)
-  | _                   => throwUnsupportedSyntax
+  | `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do
+    let r ← elabTermEnsuringType e type
+    logUnassignedAndAbort (← getMVars r)
+    return r
+  | _ => throwUnsupportedSyntax
 
 def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
   let val ← elabTermEnsuringType stx expectedType?
@@ -53,7 +60,7 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix :
     else
       let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural
       let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural
-      discard <| Term.logUnassignedUsingErrorInfos naturalMVarIds
+      logUnassignedAndAbort naturalMVarIds
       pure syntheticMVarIds.toList
   tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
   pure (val, newMVarIds)

tests/lean/exactErrorPos.lean

@@ -0,0 +1,19 @@
+set_option pp.rawOnError true
+
+theorem ex1 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by
+  exact h1 _ _
+
+theorem ex2 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by
+  refine h1 _ _
+
+theorem ex3 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by
+  first | exact h1 _ _ | apply h1
+  assumption
+
+theorem ex4 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by
+  first | refine h1 _ _ | apply h1
+  assumption
+
+theorem ex5 (f g : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) (h3 : g x = x) : f x = x := by
+  first | apply h3 | apply h1
+  assumption

tests/lean/exactErrorPos.lean.expected.out

@@ -0,0 +1,26 @@
+exactErrorPos.lean:4:13-4:14: error: don't know how to synthesize placeholder
+context:
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ x > 0
+exactErrorPos.lean:3:99-4:14: error: unsolved goals
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ f x = x
+exactErrorPos.lean:7:14-7:15: error: don't know how to synthesize placeholder
+context:
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ x > 0
+exactErrorPos.lean:6:99-7:15: error: unsolved goals
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ f x = x