max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve split tactic error message

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-23 16:00:42 -08:00
parent 902e60c480
commit c491659970
3 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Tactic/Split.lean
View file

@ -20,12 +20,12 @@ open Meta
throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
if simplifyTarget then
liftMetaTactic fun mvarId => do
let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
return mvarIds
else
let fvarId ← getFVarId hyps[0]
liftMetaTactic fun mvarId => do
let some mvarIds ← splitLocalDecl? mvarId fvarId | throwError "'split' tactic failed"
let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId ""
return mvarIds
| Location.wildcard =>
liftMetaTactic fun mvarId => do
@ -33,7 +33,7 @@ open Meta
for fvarId in fvarIds do
if let some mvarIds ← splitLocalDecl? mvarId fvarId then
return mvarIds
let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
return mvarIds
end Lean.Elab.Tactic

11
src/Lean/Message.lean
View file

@ -59,6 +59,17 @@ inductive MessageData where
namespace MessageData
partial def isEmpty : MessageData → Bool
| ofFormat f => f.isEmpty
| withContext _ m => m.isEmpty
| withNamingContext _ m => m.isEmpty
| nest _ m => m.isEmpty
| group m => m.isEmpty
| compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty
| tagged _ m => m.isEmpty
| node ms => ms.all (·.isEmpty)
| _ => false
/- Instantiate metavariables occurring in nexted `ofExpr` constructors.
It uses the surrounding `MetavarContext` at `withContext` constructors.
-/

5
src/Lean/Meta/Tactic/Util.lean
View file

@ -28,7 +28,10 @@ def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous)
mkFreshExprMVar type MetavarKind.syntheticOpaque tag
def throwTacticEx {α} (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ref := Syntax.missing) : MetaM α :=
throwError "tactic '{tacticName}' failed, {msg}\n{MessageData.ofGoal mvarId}"
if msg.isEmpty then
throwError "tactic '{tacticName}' failed\n{MessageData.ofGoal mvarId}"
else
throwError "tactic '{tacticName}' failed, {msg}\n{MessageData.ofGoal mvarId}"
def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"