From dfe8ad0ac23ea368fdaecc2fec44c5d5206f57bc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:41 +0100 Subject: [PATCH 1/3] Improve `LocalContext` and `LocalInstance` extraction for sorries --- REPL/Main.lean | 8 ++------ REPL/Snapshots.lean | 49 +++++++++++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 25 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 9b36b27d..c1b0c717 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op fun ⟨ctx, g, pos, endPos⟩ => do let (goal, proofState) ← match g with | .tactic g => do - let lctx ← ctx.runMetaM {} do - match ctx.mctx.findDecl? g with - | some decl => return decl.lctx - | none => throwError "unknown metavariable '{g}'" - let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals? + let s ← ProofSnapshot.create ctx none env? [g] rootGoals? pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term lctx (some t) => do let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] @@ -197,7 +193,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do unless (← Meta.isDefEq pft expectedType) do return s!"Error: proof has type {pft} but root goal has type {expectedType}" - let pf ← abstractAllLambdaFVars pf + let pf ← abstractAllLambdaFVars pf >>= instantiateMVars let pft ← Meta.inferType pf >>= instantiateMVars if pf.hasExprMVar then diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index eaebffc4..7f422dff 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·) + /-- Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals. - 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) (env? : Option Environment) (goals : List MVarId) (rootGoals? : Option (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)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } - pure <| - { coreState := s - coreContext := ← readThe Core.Context - metaState := ← getThe Meta.State - metaContext := ← readThe Meta.Context - termState := {} - termContext := {} - tacticState := { goals } - tacticContext := { elaborator := .anonymous } - rootGoals := match rootGoals? with - | none => goals - | some gs => gs } + -- Get the local context from the goals if not provided. + let lctx ← match lctx? with + | none => match goals with + | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx + | [] => match rootGoals? with + | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx + | _ => pure {} + | some lctx => pure lctx + + ctx.runMetaM lctx do + -- update local instances, which is necessary when `types` is non-empty + Meta.withLocalInstances (lctx.decls.toList.filterMap id) do + let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) + let s ← getThe Core.State + let s := match env? with + | none => s + | some env => { s with env } + pure <| + { coreState := s + coreContext := ← readThe Core.Context + metaState := ← getThe Meta.State + metaContext := ← readThe Meta.Context + termState := {} + termContext := {} + tacticState := { goals } + tacticContext := { elaborator := .anonymous } + rootGoals := match rootGoals? with + | none => goals + | some gs => gs } open Lean.Core in /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/ From dc85fc545fc80dccacff254dd0516adfcd212bfc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:42 +0100 Subject: [PATCH 2/3] Add test --- test/local_instance_proof.expected.out | 62 ++++++++++++++++++++++++++ test/local_instance_proof.in | 21 +++++++++ 2 files changed, 83 insertions(+) create mode 100644 test/local_instance_proof.expected.out create mode 100644 test/local_instance_proof.in diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out new file mode 100644 index 00000000..5a93d082 --- /dev/null +++ b/test/local_instance_proof.expected.out @@ -0,0 +1,62 @@ +{"env": 0} + +{"env": 1} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 42}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 47}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"sorries": + [{"proofState": 2, + "pos": {"line": 1, "column": 45}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 50}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 3} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"env": 4} + +{"sorries": + [{"proofState": 4, + "pos": {"line": 1, "column": 17}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 22}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 5} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + +{"sorries": + [{"proofState": 6, + "pos": {"line": 1, "column": 20}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 25}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 6} + +{"proofStatus": "Completed", "proofState": 7, "goals": []} + diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in new file mode 100644 index 00000000..eeefd5ef --- /dev/null +++ b/test/local_instance_proof.in @@ -0,0 +1,21 @@ +{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 2} + +{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0} + +{"cmd": "def test2 : α := sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 4} + +{"cmd": "def test2 : α := by sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 6} From 8b709807c902e0ec3fc272abe50f0081e5d40067 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 29 Jan 2026 13:06:27 +0100 Subject: [PATCH 3/3] Fix test v4.28.0-rc1 --- test/local_instance_proof.expected.out | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out index 5a93d082..a3c25109 100644 --- a/test/local_instance_proof.expected.out +++ b/test/local_instance_proof.expected.out @@ -11,7 +11,7 @@ [{"severity": "warning", "pos": {"line": 1, "column": 4}, "endPos": {"line": 1, "column": 9}, - "data": "declaration uses 'sorry'"}], + "data": "declaration uses `sorry`"}], "env": 2} {"proofStatus": "Completed", "proofState": 1, "goals": []} @@ -25,7 +25,7 @@ [{"severity": "warning", "pos": {"line": 1, "column": 4}, "endPos": {"line": 1, "column": 9}, - "data": "declaration uses 'sorry'"}], + "data": "declaration uses `sorry`"}], "env": 3} {"proofStatus": "Completed", "proofState": 3, "goals": []} @@ -41,7 +41,7 @@ [{"severity": "warning", "pos": {"line": 1, "column": 4}, "endPos": {"line": 1, "column": 9}, - "data": "declaration uses 'sorry'"}], + "data": "declaration uses `sorry`"}], "env": 5} {"proofStatus": "Completed", "proofState": 5, "goals": []} @@ -55,7 +55,7 @@ [{"severity": "warning", "pos": {"line": 1, "column": 4}, "endPos": {"line": 1, "column": 9}, - "data": "declaration uses 'sorry'"}], + "data": "declaration uses `sorry`"}], "env": 6} {"proofStatus": "Completed", "proofState": 7, "goals": []}