Fix failure detection for TacGens

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

Fixes #125

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 $

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

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