feat: print remaining safe goals in terminal mode (#139)

Co-authored-by: Jannis Limperg <[email protected]>

Aesop/Search/Main.lean

@@ -217,6 +217,32 @@ def treeHasProgress : TreeM Bool := do
     (.mvarCluster (← get).root)
   resultRef.get
 
+def throwAesopEx (mvarId : MVarId) (remainingSafeGoals : Array MVarId)
+    (safePrefixExpansionSuccess : Bool) (msg? : Option MessageData) :
+    SearchM Q α := do
+  if aesop.smallErrorMessages.get (← getOptions) then
+    match msg? with
+    | none => throwError "tactic 'aesop' failed"
+    | some msg => throwError "tactic 'aesop' failed, {msg}"
+  else
+    let maxRapps := (← read).options.maxSafePrefixRuleApplications
+    let suffix :=
+      if remainingSafeGoals.isEmpty then
+        m!""
+      else
+        let gs := .joinSep (remainingSafeGoals.toList.map toMessageData) "\n\n"
+        let suffix' :=
+          if safePrefixExpansionSuccess then
+            m!""
+          else
+            m!"\nThe safe prefix was not fully expanded because the maximum number of rule applications ({maxRapps}) was reached."
+        m!"\nRemaining goals after safe rules:{indentD gs}{suffix'}"
+    -- Copy-pasta from `Lean.Meta.throwTacticEx`
+    match msg? with
+    | none => throwError "tactic 'aesop' failed\nInitial goal:{indentD mvarId}{suffix}"
+    | some msg => throwError "tactic 'aesop' failed, {msg}\nInitial goal:{indentD mvarId}{suffix}"
+
+
 -- When we hit a non-fatal error (i.e. the search terminates without a proof
 -- because the root goal is unprovable or because we hit a search limit), we
 -- usually:
@@ -230,29 +256,25 @@ def treeHasProgress : TreeM Bool := do
 -- not expand the safe rules after the fact, the tactic's output would be
 -- sensitive to minor changes in, e.g., rule priority.
 def handleNonfatalError (err : MessageData) : SearchM Q (Array MVarId) := do
-  let opts := (← read).options
-  if opts.terminal then
-    throwAesopEx (← getRootMVarId) err
   let safeExpansionSuccess ← expandSafePrefix
-  if ! safeExpansionSuccess then
-    logWarning m!"aesop: safe prefix was not fully expanded because the maximum number of rule applications ({(← read).options.maxSafePrefixRuleApplications}) was reached."
-  if ! (← treeHasProgress) then
-    throwAesopEx (← getRootMVarId) "made no progress"
-  if opts.warnOnNonterminal then
-    logWarning m!"aesop: {err}"
-  let goals ← extractSafePrefix
+  let safeGoals ← extractSafePrefix
   aesop_trace[proof] do
     match ← getProof? with
     | some proof =>
       (← getRootMVarId).withContext do
         aesop_trace![proof] "{proof}"
     | none => aesop_trace![proof] "<no proof>"
   traceTree
-  return goals
-
-def handleFatalError (e : Exception) : SearchM Q α := do
-  traceTree
-  throw e
+  let opts := (← read).options
+  if opts.terminal then
+    throwAesopEx (← getRootMVarId) safeGoals safeExpansionSuccess err
+  if ! (← treeHasProgress) then
+    throwAesopEx (← getRootMVarId) #[] safeExpansionSuccess "made no progress"
+  if opts.warnOnNonterminal then
+    logWarning m!"aesop: {err}"
+  if ! safeExpansionSuccess then
+    logWarning m!"aesop: safe prefix was not fully expanded because the maximum number of rule applications ({(← read).options.maxSafePrefixRuleApplications}) was reached."
+  return safeGoals
 
 partial def searchLoop : SearchM Q (Array MVarId) :=
   withIncRecDepth do
@@ -288,7 +310,6 @@ def search (goal : MVarId) (ruleSet? : Option LocalRuleSet := none)
     SearchM.run ruleSet options simpConfig simpConfigSyntax? goal stats do
       show SearchM Q _ from
       try searchLoop
-      catch e => handleFatalError e
       finally freeTree
   return (goals, stats)
 

Aesop/Util/Basic.lean

@@ -374,12 +374,4 @@ register_option aesop.smallErrorMessages : Bool := {
     descr := "(aesop) Print smaller error messages. Used for testing."
   }
 
-def throwAesopEx (mvarId : MVarId) (msg? : Option MessageData) : MetaM α := do
-  if aesop.smallErrorMessages.get (← getOptions) then
-    match msg? with
-    | none => throwError "tactic 'aesop' failed"
-    | some msg => throwError "tactic 'aesop' failed, {msg}"
-  else
-    throwTacticEx `aesop mvarId msg?
-
 end Aesop

AesopTest/RulePattern.lean

@@ -51,7 +51,8 @@ axiom falso' : True → False
 
 /--
 error: tactic 'aesop' failed, made no progress
-⊢ False
+Initial goal:
+  ⊢ False
 -/
 #guard_msgs in
 example : False := by

AesopTest/SafePrefixExpansionRappLimit.lean

@@ -10,14 +10,27 @@ import Aesop
 axiom loopy {α : Prop} : α ∨ α → α
 
 /--
-warning: aesop: safe prefix was not fully expanded because the maximum number of rule applications (50) was reached.
----
 warning: aesop: failed to prove the goal. Some goals were not explored because the maximum rule application depth (30) was reached. Set option 'maxRuleApplicationDepth' to increase the limit.
 ---
+warning: aesop: safe prefix was not fully expanded because the maximum number of rule applications (50) was reached.
+---
 error: unsolved goals
 case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a
 ⊢ False
 -/
 #guard_msgs in
-example : false := by
+example : False := by
   aesop
+
+/--
+error: tactic 'aesop' failed, failed to prove the goal. Some goals were not explored because the maximum rule application depth (30) was reached. Set option 'maxRuleApplicationDepth' to increase the limit.
+Initial goal:
+  ⊢ False
+Remaining goals after safe rules:
+  case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a
+  ⊢ False
+The safe prefix was not fully expanded because the maximum number of rule applications (50) was reached.
+-/
+#guard_msgs in
+example : False := by
+  aesop (config := { terminal := true })

AesopTest/SafePrefixInTerminalError.lean

@@ -0,0 +1,13 @@
+import Aesop
+
+/--
+error: tactic 'aesop' failed, failed to prove the goal after exhaustive search.
+Initial goal:
+  ⊢ ∀ (a b : Nat), a + b = b + 2 * a
+Remaining goals after safe rules:
+  a b : Nat
+  ⊢ a + b = b + 2 * a
+-/
+#guard_msgs in
+example : ∀ (a b : Nat), a + b = b + 2 * a := by
+  aesop (config := { terminal := true })

AesopTest/TerminalError.lean

@@ -10,7 +10,10 @@ set_option aesop.check.all true
 
 /--
 error: tactic 'aesop' failed, failed to prove the goal after exhaustive search.
-⊢ False
+Initial goal:
+  ⊢ False
+Remaining goals after safe rules:
+  ⊢ False
 -/
 #guard_msgs in
 example : False := by

AesopTest/TraceProof.lean

@@ -13,6 +13,8 @@ set_option trace.aesop.proof true
 
 /--
 error: tactic 'aesop' failed, made no progress
+---
+info: [aesop.proof] <no proof>
 -/
 #guard_msgs in
 example : α := by