synthesizeSyntheticMVarsNoPostponing

Author: kim-em

REPL/Lean/InfoTree.lean

@@ -200,12 +200,9 @@ Finds all appearances of `sorry` in an `InfoTree`, reporting
 -/
 def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Position) :=
   (t.findSorryTacticNodes.map fun ⟨i, ctx⟩ =>
-    if i.goalsBefore.isEmpty then
-      dbgTrace "no goals at sorry!" fun _ => (ctx, panic "")
-    else
-      -- HACK: creating a child ngen
-      ({ ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, .tactic i.goalsBefore.head!,
-        stxRange ctx.fileMap i.stx)) ++
+    -- HACK: creating a child ngen
+    ({ ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, .tactic i.goalsBefore.head!,
+      stxRange ctx.fileMap i.stx)) ++
   (t.findSorryTermNodes.map fun ⟨i, ctx⟩ =>
     (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx))
 

REPL/Snapshots.lean

@@ -139,7 +139,8 @@ def runMetaM (p : ProofSnapshot) (t : MetaM α) : IO (α × ProofSnapshot) := do
 
 /-- Run a `TermElabM` monadic function in the current `ProofSnapshot`, updating the `Term.State`. -/
 def runTermElabM (p : ProofSnapshot) (t : TermElabM α) : IO (α × ProofSnapshot) := do
-  let ((a, termState), p') ← p.runMetaM (Lean.Elab.Term.TermElabM.run (s := p.termState) do t)
+  let ((a, termState), p') ← p.runMetaM (Lean.Elab.Term.TermElabM.run (s := p.termState)
+    (do let r ← t; Term.synthesizeSyntheticMVarsNoPostponing; pure r))
   return (a, { p' with termState })
 
 /-- Run a `TacticM` monadic function in the current `ProofSnapshot`, updating the `Tactic.State`. -/

test/Mathlib/test/20240209.expected.out

@@ -0,0 +1,22 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 22},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 27}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofState": 1,
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "unsolved goals\n⊢ False"}],
+ "goals": []}
+

test/Mathlib/test/20240209.in

@@ -0,0 +1,5 @@
+{"cmd": "import Std.Tactic.Simpa"}
+
+{"cmd": "example : False := by sorry", "env": 0}
+
+{"tactic": "simpa using show False by done", "proofState": 0}

test/Mathlib/test/20240209.lean

@@ -0,0 +1,4 @@
+import Std.Tactic.Simpa
+
+example : False := by
+  simpa using show False by done