From 1bbc601de6ff7b69fee3c028069879e830baa0e8 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Thu, 23 May 2024 21:01:45 +0200
Subject: [PATCH] Fix failure detection for TacGens

... in the presence of delayed-assigned mvars.

Fixes #125
---
 Aesop/RuleTac/Tactic.lean |  2 +-
 Aesop/Util/Basic.lean     | 12 ++++++++++++
 AesopTest/125.lean        | 17 +++++++++++++++++
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 AesopTest/125.lean

diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean
index 7a7bf797..cbf25024 100644
--- a/Aesop/RuleTac/Tactic.lean
+++ b/Aesop/RuleTac/Tactic.lean
@@ -79,7 +79,7 @@ unsafe def tacGenImpl (decl : Name) : RuleTac := λ input => do
       let goals := (← run input.goal (evalTactic stx) |>.run').toArray
       let postState ← saveState
       if let some proof ← getExprMVarAssignment? input.goal then
-        if (← instantiateMVars proof).hasSorry then
+        if ← hasSorry proof then
           throwError "generated proof contains sorry"
       let scriptBuilder? :=
         mkScriptBuilder? input.options.generateScript $
diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
index 7d8944a3..48291d7c 100644
--- a/Aesop/Util/Basic.lean
+++ b/Aesop/Util/Basic.lean
@@ -197,6 +197,18 @@ def updateSimpEntryPriority (priority : Nat) (e : SimpEntry) : SimpEntry :=
   | .thm t => .thm { t with priority }
   | .toUnfoldThms .. | .toUnfold .. => e
 
+partial def hasSorry (e : Expr) : MetaM Bool :=
+  (·.isSome) <$> e.findM? λ
+    | .mvar mvarId => do
+      if let some ass ← getDelayedMVarAssignment? mvarId then
+        hasSorry $ .mvar ass.mvarIdPending
+      else if let some ass ← getExprMVarAssignment? mvarId then
+        hasSorry ass
+      else
+        return false
+    | .const ``sorryAx _ => return true
+    | _ => return false
+
 def isAppOfUpToDefeq (f : Expr) (e : Expr) : MetaM Bool :=
   withoutModifyingState do
     let type ← inferType f
diff --git a/AesopTest/125.lean b/AesopTest/125.lean
new file mode 100644
index 00000000..eb133b23
--- /dev/null
+++ b/AesopTest/125.lean
@@ -0,0 +1,17 @@
+import Aesop
+
+set_option aesop.check.all true
+set_option aesop.smallErrorMessages true
+
+@[aesop 90%]
+def myTacGen : Aesop.TacGen := fun _ => do
+  return #[("exact ⟨val - f { val := val, property := property }, fun a ha => by simpa⟩",
+            0.9)]
+
+/-- error: tactic 'aesop' failed, made no progress -/
+#guard_msgs in
+theorem foo (f : { x // 0 < x } → { x // 0 < x }) (val : Nat)
+    (property : 0 < val) :
+    ∃ w x, ∀ (a : Nat) (b : 0 < a), ↑(f { val := a, property := b }) = w * a + x := by
+  constructor
+  aesop