feat: use environment from before the declaration, so exact? doesn't give circular proofs

Author: kim-em

REPL/Main.lean

@@ -95,15 +95,15 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
-def sorries (trees : List InfoTree) : M m (List Sorry) :=
+def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) :=
   trees.bind InfoTree.sorries |>.mapM
     fun ⟨ctx, g, pos, endPos⟩ => do
       let (goal, proofState) ← match g with
       | .tactic g => do
-         let s ← ProofSnapshot.create ctx none [g]
+         let s ← ProofSnapshot.create ctx none env? [g]
          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
       | .term lctx (some t) => do
-         let s ← ProofSnapshot.create ctx lctx [] [t]
+         let s ← ProofSnapshot.create ctx lctx env? [] [t]
          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
       | .term _ none => unreachable!
       let proofStateId ← proofState.mapM recordProofSnapshot
@@ -118,7 +118,7 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
 def tactics (trees : List InfoTree) : M m (List Tactic) :=
   trees.bind InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, goals, pos, endPos⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none goals)
+      let proofState := some (← ProofSnapshot.create ctx none none goals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
@@ -139,7 +139,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   | none => pure trees
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees
+  let sorries ← sorries trees none
   let id ← recordProofSnapshot proofState
   return {
     proofState := id
@@ -194,15 +194,15 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     | none => pure (none, true)
   if notFound then
     return .inr ⟨"Unknown environment."⟩
-  let cmdState? := cmdSnapshot?.map fun c => c.cmdState
+  let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
   let (cmdState, messages, trees) ← try
-    IO.processInput s.cmd cmdState?
+    IO.processInput s.cmd initialCmdState?
   catch ex =>
     return .inr ⟨ex.toString⟩
   let messages ← messages.mapM fun m => Message.of m
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees
+  let sorries ← sorries trees (initialCmdState?.map (·.env))
   let tactics ← match s.allTactics with
   | some true => tactics trees
   | _ => pure []

REPL/Snapshots.lean

@@ -189,13 +189,17 @@ Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, an
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
-def create (ctx : ContextInfo) (lctx? : Option LocalContext)
+def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
     (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
     goals.head!.withContext do
+    let s ← getThe Core.State
+    let s := match env? with
+    | none => s
+    | some env => { s with env }
     pure <|
-    { coreState := ← getThe Core.State
+    { coreState := s
       coreContext := ← readThe Core.Context
       metaState := ← getThe Meta.State
       metaContext := ← readThe Meta.Context

test/Mathlib/test/exact.expected.out

@@ -0,0 +1,37 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 27},
+   "goal": "⊢ 0 < 1",
+   "endPos": {"line": 1, "column": 32}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 12},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofState": 1,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "Try this: exact Nat.le.refl"}],
+ "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 27},
+   "goal": "⊢ 3 = 7",
+   "endPos": {"line": 1, "column": 32}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 12},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"message":
+ "Lean error:\n`exact?` could not close the goal. Try `apply?` to see partial suggestions."}
+

test/Mathlib/test/exact.in

@@ -0,0 +1,10 @@
+{"cmd": "import Mathlib\n\nset_option maxHeartbeats 500000"}
+
+{"cmd": "theorem test : 0 < 1 := by sorry", "env": 0}
+
+{"tactic": "exact?", "proofState": 0}
+
+{"cmd": "theorem test : 3 = 7 := by sorry", "env": 0}
+
+{"tactic": "exact?", "proofState": 2}
+