Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev

Reviewed-on: #141

Pantograph/Library.lean

@@ -138,16 +138,35 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
-  runMetaM do
+  : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
+
+  let root? ← if rootExpr then
+      state.rootExpr?.mapM λ expr => state.withRootContext do
+        serializeExpression options (← instantiateAll expr)
+    else
+      pure .none
+  let parent? ← if parentExpr then
+      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? := ← state.rootExpr?.mapM (λ expr =>
+    root?,
-        state.withRootContext do
+    parent?,
-          serializeExpression options (← instantiateAll expr)),
+    goals,
-      parent? := ← state.parentExpr?.mapM (λ expr =>
+    extraMVars,
-        state.withParentContext do
-          serializeExpression options (← instantiateAll expr)),
   }
 
 @[export pantograph_goal_tactic_m]

Pantograph/Protocol.lean

@@ -271,12 +271,23 @@ 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
+  parent?: Option Expression := .none
+  goals: Array Goal := #[]
+  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Repl.lean

@@ -223,7 +223,13 @@ 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 goalState state.options
+    let result ← runMetaInMainM <| goalPrint
+        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)]
+    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
      ({ 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
+## Caveats and Limitations
 
 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,7 +38,20 @@ 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.
+  paradigms. However, if there are tactics which perform non-trivial operations
+  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