Compare commits

..

8 Commits

5 changed files with 65 additions and 16 deletions

View File

@ -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 :=
runMetaM do
def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
: 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 =>
state.withRootContext do
serializeExpression options (← instantiateAll expr)),
parent? := ← state.parentExpr?.mapM (λ expr =>
state.withParentContext do
serializeExpression options (← instantiateAll expr)),
root?,
parent?,
goals,
extraMVars,
}
@[export pantograph_goal_tactic_m]

View File

@ -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

View File

@ -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

View File

@ -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),

View File

@ -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