Add Pantograph-like approach to tactic mode

README.md

@@ -44,7 +44,8 @@ Example output:
 {"sorries":
  [{"pos": {"line": 1, "column": 18},
    "endPos": {"line": 1, "column": 23},
-   "goal": "⊢ Nat",
+   "parentDecl": "h",
+   "goals": ["⊢ Nat"],
    "proofState": 0}],
  "messages":
  [{"severity": "error",
@@ -92,12 +93,13 @@ and then use the `proofState` index returned for each `sorry`.
 
 Example usage:
 ```json
-{"cmd" : "def f (x : Unit) : Nat := by sorry"}
+{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries": "individual"}
 
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 29},
-   "goal": "x : Unit\n⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["x : Unit\n⊢ Nat"],
    "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",

REPL/JSON.lean

@@ -13,7 +13,8 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
-  rootGoals : Option Bool := none
+  -- Should be "individual", "grouped", or "rootGoals".
+  sorries : Option String := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
@@ -76,28 +77,32 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
 structure Sorry where
   pos : Pos
   endPos : Pos
-  goal : String
+  goals : List String
   /--
   The index of the proof state at the sorry.
   You can use the `ProofStep` instruction to run a tactic at this state.
   -/
   proofState : Option Nat
+  parentDecl: Option Name := none
 deriving FromJson
 
 instance : ToJson Sorry where
   toJson r := Json.mkObj <| .flatten [
-    [("goal", r.goal)],
+    [("goals", toJson r.goals)],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
     if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
+    if r.parentDecl.isSome then [("parentDecl", toJson r.parentDecl)] else []
   ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
-def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
+def Sorry.of (goals : List String) (pos endPos : Lean.Position) (proofState : Option Nat)
+(parentDecl : Option Name): Sorry :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
-    goal,
-    proofState }
+    goals,
+    proofState,
+    parentDecl }
 
 structure Tactic where
   pos : Pos
@@ -106,16 +111,19 @@ structure Tactic where
   tactic : String
   proofState : Option Nat
   usedConstants : Array Name
+  parentDecl : Option Name := none
 deriving ToJson, FromJson
 
 /-- Construct the JSON representation of a Lean tactic. -/
-def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) (usedConstants : Array Name) : Tactic :=
+def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat)
+(usedConstants : Array Name) (parentDecl : Option Name) : Tactic :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
     goals,
     tactic,
     proofState,
-    usedConstants }
+    usedConstants,
+    parentDecl }
 
 /--
 A response to a Lean command.
@@ -150,7 +158,6 @@ structure ProofStepResponse where
   proofState : Nat
   goals : List String
   messages : List Message := []
-  sorries : List Sorry := []
   traces : List String
   proofStatus : String
 deriving ToJson, FromJson
@@ -160,7 +167,6 @@ instance : ToJson ProofStepResponse where
     [("proofState", r.proofState)],
     [("goals", toJson r.goals)],
     Json.nonemptyList "messages" r.messages,
-    Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces,
     [("proofStatus", r.proofStatus)]
   ]

REPL/Lean/InfoTree.lean

@@ -195,18 +195,18 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa
   | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals)
   | _ => none
 
-/-- Returns the root goals for a given `InfoTree`. -/
-partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
-  List (TacticInfo × ContextInfo × List MVarId) :=
+/-- Returns the root and last goals for a given `InfoTree`. -/
+partial def findRootAndLastGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
+    List (TacticInfo × ContextInfo × List MVarId × List MVarId) :=
   match t with
-  | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?)
+  | .context ctx t => t.findRootAndLastGoals (ctx.mergeIntoOuter? ctx?)
   | .node info ts =>
     match info with
     | .ofTacticInfo i =>
       match ctx? with
-      | some ctx => [(i, ctx, i.goalsBefore)]
+      | some ctx => [(i, ctx, i.goalsBefore, i.goalsAfter)]
       | _ => []
-    | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?)
+    | _ => ts.toList.flatMap (fun t => t.findRootAndLastGoals ctx?)
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree`
@@ -264,12 +264,21 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List
       i.getUsedConstantsAsSet.toArray )
 
 def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
-  t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
+  t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, _⟩ =>
     let range := stxRange ctx.fileMap i.stx
     ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
       rootGoals,
       range.fst )
 
+def rootAndLastGoals (t : InfoTree) : List (ContextInfo × List MVarId × List MVarId × Position × Position) :=
+  t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, lastGoals⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxAfter, ngen := ctx.ngen.mkChild.1 },
+      rootGoals,
+      lastGoals,
+      range.fst,
+      range.snd )
+
 end Lean.Elab.InfoTree
 
 namespace Lean.Elab.TacticInfo

REPL/Main.lean

@@ -100,20 +100,33 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
     | .term _ none => false
     | _ => true ) |>.mapM
       fun ⟨ctx, g, pos, endPos⟩ => do
-        let (goal, proofState) ← match g with
+        let (goals, 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?
-          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          pure ((← s.ppGoals).map (s!"{·}"), some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
-          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          pure ((← s.ppGoals).map (s!"{·}"), some s)
         | .term _ none => unreachable!
         let proofStateId ← proofState.mapM recordProofSnapshot
-        return Sorry.of goal pos endPos proofStateId
+        return Sorry.of goals pos endPos proofStateId ctx.parentDecl?
+
+def groupedSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
+  let a ← trees.flatMap InfoTree.rootAndLastGoals |>.mapM
+    fun ⟨ctx, rootGoals, lastGoals, startPos, endPos⟩ => do
+      let proofState ← ProofSnapshot.create ctx none env? lastGoals rootGoals
+      let proofState' ← proofState.runString "skip" -- Trick to get the sorries
+      let goals := (← proofState'.ppGoals).map (s!"{·}")
+      if goals.isEmpty then
+        return []
+      else
+        let proofStateId ← recordProofSnapshot proofState'
+        return [Sorry.of goals startPos endPos proofStateId ctx.parentDecl?]
+  return a.flatten
 
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
@@ -128,15 +141,15 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
-      return Tactic.of goals tactic pos endPos proofStateId ns
+      return Tactic.of goals tactic pos endPos proofStateId ns ctx.parentDecl?
 
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none env? goals goals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let goals ← goals.mapM (fun g => do pure s!"{(← ctx.ppGoals [g])}".trim)
       let proofStateId ← proofState.mapM recordProofSnapshot
-      return Sorry.of goals pos pos proofStateId
+      return Sorry.of goals pos ⟨0,0⟩ proofStateId ctx.parentDecl?
 
 
 private def collectFVarsAux : Expr → NameSet
@@ -200,6 +213,8 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             let pf ← abstractAllLambdaFVars pf
             let pft ← Meta.inferType pf >>= instantiateMVars
 
+            if pf.hasSorry then
+              return "Incomplete: contains sorry"
             if pf.hasExprMVar then
               return "Incomplete: contains metavariable(s)"
 
@@ -220,9 +235,6 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
               let _ ← addDecl decl
             catch ex =>
               return s!"Error: kernel type check failed: {← ex.toMessageData.toString}"
-
-            if pf.hasSorry then
-              return "Incomplete: contains sorry"
             return "Completed"
 
         | _ => return "Not verified: more than one initial goal"
@@ -236,22 +248,11 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   let messages := proofState.newMessages old?
   let messages ← messages.mapM fun m => Message.of m
   let traces ← proofState.newTraces old?
-  let trees := proofState.newInfoTrees old?
-  let trees ← match old? with
-  | some old => do
-    let (ctx, _) ← old.runMetaM do return { ← CommandContextInfo.save with }
-    let ctx := PartialContextInfo.commandCtx ctx
-    pure <| trees.map fun t => InfoTree.context ctx t
-  | 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 none (some proofState.rootGoals)
   let id ← recordProofSnapshot proofState
   return {
     proofState := id
-    goals := (← proofState.ppGoals).map fun s => s!"{s}"
+    goals := (← proofState.ppGoals).map (s!"{·}")
     messages
-    sorries
     traces
     proofStatus := (← getProofStatus proofState) }
 
@@ -309,10 +310,11 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   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 initialCmdState.env none
-  let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
-  | _ => pure sorries
+  let sorries ← match s.sorries with
+  | some "individual" => sorries trees initialCmdState.env none
+  | some "grouped" => groupedSorries trees initialCmdState.env
+  | some "rootGoals" => collectRootGoalsAsSorries trees initialCmdState.env
+  | _ => pure []
   let tactics ← match s.allTactics with
   | some true => tactics trees initialCmdState.env
   | _ => pure []
@@ -350,8 +352,10 @@ def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
 
 /--
 Run a single tactic, returning the id of the new proof statement, and the new goals.
+This implementation supports branching in tactic proofs.
+When a tactic generates new goals, each goal is properly tracked to allow subsequent tactics to be
+applied.
 -/
--- TODO detect sorries?
 def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do
   match (← get).proofStates[s.proofState]? with
   | none => return .inr ⟨"Unknown proof state."⟩

REPL/Snapshots.lean

@@ -114,6 +114,20 @@ namespace ProofSnapshot
 
 open Lean Elab Tactic
 
+/-- Transform `sorry` expressions into fresh opaque metavariables, collecting their IDs. -/
+def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr :=
+  Meta.transform src λ expr =>
+    if expr.isSorry then do
+      -- extract the proof type from `sorry` (the first binder argument)
+      let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
+      if type.hasSorry then
+        throwError s!"Nested sorry in type not supported: {← Meta.ppExpr type}"
+      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+      modify (mvar.mvarId! :: ·)
+      pure $ .done mvar
+    else
+      pure .continue
+
 /-- New messages in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List Lean.Message :=
   match old? with
@@ -180,7 +194,27 @@ and run it in the current `ProofSnapshot`.
 def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
   match Parser.runParserCategory p.coreState.env `tactic t with
   | .error e => throw (IO.userError e)
-  | .ok stx => p.runSyntax stx
+  | .ok stx => do
+    let result ← p.runSyntax stx
+
+    -- Process all goals after tactic execution to find and transform any sorries
+    let (newGoals, result') ← result.runMetaM do
+      let processExpr (acc : List MVarId) (mvarId : MVarId) (expr : Expr) : MetaM (List MVarId) := do
+        if expr.hasSorry then
+          mvarId.withContext do
+            let (newExpr, exprHoles) ← sorryToHole expr |>.run []
+            mvarId.assign newExpr
+            pure (acc ++ exprHoles)
+        else
+          pure acc
+
+      -- Process all expressions in the metavariable context
+      let mctx := result.metaState.mctx
+      let exprHoles ← mctx.eAssignment.foldlM processExpr []
+      pure exprHoles
+
+    let combinedGoals := newGoals ++ result'.tacticState.goals
+    return { result' with tacticState := { goals := combinedGoals } }
 
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=

test/Mathlib/test/20240209.expected.out

@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
+   "parentDecl": "_example",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
@@ -10,12 +11,12 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 1,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\n⊢ False"}],
- "goals": []}
+ "goals": ["⊢ False"]}
 

test/Mathlib/test/20240209.in

@@ -1,3 +1,3 @@
-{"cmd": "example : False := by sorry"}
+{"cmd": "example : False := by sorry", "sorries": "individual"}
 
 {"tactic": "simpa using show False by done", "proofState": 0}

test/Mathlib/test/H20231115.expected.out

@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Nat\n⊢ x + 1 > x",
+   "parentDecl": "_example",
+   "goals": ["x : Nat\n⊢ x + 1 > x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",

test/Mathlib/test/H20231115.in

@@ -1,5 +1,5 @@
 {"cmd": "import Mathlib.Tactic.Cases"}
 
-{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0}
+{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "induction' x with x hx", "proofState": 0}