Pantograph/Library.lean

@@ -138,36 +138,17 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
-  : CoreM Protocol.GoalPrintResult := runMetaM do
+  runMetaM do
-  state.restoreMetaM
+    state.restoreMetaM
-
+    return {
-  let root? ← if rootExpr then
+      root? := ← state.rootExpr?.mapM (λ expr =>
-      state.rootExpr?.mapM λ expr => state.withRootContext do
+        state.withRootContext do
-        serializeExpression options (← instantiateAll expr)
+          serializeExpression options (← instantiateAll expr)),
-    else
+      parent? := ← state.parentExpr?.mapM (λ expr =>
-      pure .none
+        state.withParentContext do
-  let parent? ← if parentExpr then
+          serializeExpression options (← instantiateAll expr)),
-      state.parentExpr?.mapM λ expr => state.withParentContext do
+    }
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let goals ← if goals then
-      goalSerialize state options
-    else
-      pure #[]
-  let extraMVars ← extraMVars.mapM λ mvarId => do
-    let mvarId: MVarId := { name := mvarId.toName }
-    let .some _ ← mvarId.findDecl? | return {}
-    state.withContext mvarId do
-      let .some expr ← getExprMVarAssignment? mvarId | return {}
-      serializeExpression options (← instantiateAll expr)
-  return {
-    root?,
-    parent?,
-    goals,
-    extraMVars,
-  }
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=

Pantograph/Protocol.lean

@@ -271,23 +271,12 @@ structure GoalDeleteResult where
 
 structure GoalPrint where
   stateId: Nat
-
-  -- Print root?
-  rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
-  -- Print goals?
-  goals?: Option Bool := .some False
-  -- Print values of extra mvars?
-  extraMVars?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parent?: Option Expression
-  goals: Array Goal := #[]
-  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Repl.lean

@@ -223,13 +223,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint
+    let result ← runMetaInMainM <| goalPrint goalState state.options
-        goalState
-        (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
-        (goals := args.goals?.getD False)
-        (extraMVars := args.extraMVars?.getD #[])
-        (options := state.options)
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
     let state ← get

Test/Integration.lean

@@ -72,7 +72,7 @@ def test_tactic : Test :=
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
+    step "goal.print" [("stateId", .num 1)]
      ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),

doc/rationale.md

@@ -24,7 +24,7 @@ The name Pantograph is a pun. It means two things
   a locomotive. In comparison the (relatively) simple Pantograph software powers
   theorem proving projects.
 
-## Caveats and Limitations
+## Caveats
 
 Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
 flexibility it offers.  To support tree search means Pantograph has to act
@@ -38,20 +38,7 @@ differently from Lean in some times, but never at the sacrifice of soundness.
   it is supposed to finish at the end of a `by` block. Pantograph will raise the
   error in this case, since it indicates the termination of a proof search branch.
 - `pick_goal` or `swap` will not work since they run contrary to tree search
-  paradigms. However, if there are tactics which perform non-trivial operations
+  paradigms.
-  to multiple goals at the same time, this constrain could potentially be
-  relaxed at a cost of great bookkeeping overhead to the user.
-
-Pantograph cannot perform things that are inherently constrained by Lean. These
-include:
-
-- If a tactic loses track of metavariables, it will not be caught until the end
-  of the proof search. This is a bug in the tactic itself.
-- Timeouts for executing tactics is not available. Maybe this will change in the
-  future.
-- Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system.
-
 
 ## References