Pantograph.lean

@@ -114,22 +114,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match state.goalStates.find? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
     | .some goalState => do
-      let nextGoalState?: Except _ GoalState ←
+      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr?, args.have? with
-        match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
+        | .some tactic, .none, .none => do
-        | .some tactic, .none, .none, .none, .none => do
           pure ( Except.ok (← goalTactic goalState args.goalId tactic))
-        | .none, .some expr, .none, .none, .none => do
+        | .none, .some expr, .none => do
           pure ( Except.ok (← goalAssign goalState args.goalId expr))
-        | .none, .none, .some type, .none, .none => do
+        | .none, .none, .some type => do
           let binderName := args.binderName?.getD ""
           pure ( Except.ok (← goalHave goalState args.goalId binderName type))
-        | .none, .none, .none, .some pred, .none => do
+        | _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied")
-          pure ( Except.ok (← goalCalc goalState args.goalId pred))
-        | .none, .none, .none, .none, .some true => do
-          pure ( Except.ok (← goalConv goalState args.goalId))
-        | .none, .none, .none, .none, .some false => do
-          pure ( Except.ok (← goalConvExit goalState))
-        | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied")
       match nextGoalState? with
       | .error error => return .error error
       | .ok (.success nextGoalState) =>

Pantograph/Protocol.lean

@@ -202,11 +202,8 @@ structure GoalTactic where
   tactic?: Option String := .none
   expr?: Option String := .none
   have?: Option String := .none
-  calc?: Option String := .none
-  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
-  conv?: Option Bool := .none
 
-  -- In case of the `have` tactic, the new free variable name is provided here
+  -- In case of the `have` tactic, the new free variable name
   binderName?: Option String := .none
 
   deriving Lean.FromJson

README.md

@@ -81,12 +81,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
 - `options.print`: Display the current set of options
 - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
-- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr":
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
-  <expr>]}`: Execute a tactic string on a given goal. `tactic` executes an
-  ordinary tactic, `expr` assigns an expression to the current goal, `have`
-  executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step
-  of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic
-  mode.
 - `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
 - `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
 - `goal.print {"stateId": <id>}"`: Print a goal state