Pantograph.lean

@@ -20,7 +20,6 @@ structure State where
 
 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-
 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
@@ -146,17 +145,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         pure $ Except.error $ error
     match nextGoalState? with
     | .error error => return .error error
-    | .ok (.success nextGoalState) => do
+    | .ok (.success nextGoalState) =>
-      let nextGoalState ← match state.options.automaticMode, args.conv? with
-        | true, .none => do
-          let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals"
-          pure result
-        | true, .some true => pure nextGoalState
-        | true, .some false => do
-          let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
-          let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals"
-          pure result
-        | false, _ => pure nextGoalState
       let nextStateId := state.nextId
       set { state with
         goalStates := state.goalStates.insert state.nextId nextGoalState,

Pantograph/Goal.lean

@@ -27,8 +27,7 @@ structure GoalState where
   parentMVar?: Option MVarId
 
   -- Existence of this field shows that we are currently in `conv` mode.
-  -- (convRhs, goal, dormant)
+  convMVar?: Option (MVarId × MVarId) := .none
-  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
   -- Previous RHS for calc, so we don't have to repeat it every time
   -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
   calcPrevRhs?: Option (MVarId × Expr) := .none
@@ -98,20 +97,6 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
     calcPrevRhs? := .none,
   }
 
-/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume_parent]
-protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-  -- Prune parents solved goals
-  let mctx := state.mctx
-  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
-  {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := state.goals ++ parentGoals },
-    },
-  }
-
 /--
 Brings into scope a list of goals
 -/
@@ -131,6 +116,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         term := state.savedState.term,
         tactic := { goals := unassigned },
       },
+      calcPrevRhs? := .none,
     }
 /--
 Brings into scope all goals from `branch`
@@ -258,13 +244,11 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
     return (← MonadBacktrack.saveState, convMVar)
   try
     let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    -- Other goals are now dormant
-    let otherGoals := state.goals.filter $ λ g => g != goal
     return .success {
       root := state.root,
       savedState := nextSavedState
       parentMVar? := .some goal,
-      convMVar? := .some (convRhs, goal, otherGoals),
+      convMVar? := .some (convRhs, goal),
       calcPrevRhs? := .none
     }
   catch exception =>
@@ -273,7 +257,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
 /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
 protected def GoalState.convExit (state: GoalState):
       Elab.TermElabM TacticResult := do
-  let (convRhs, convGoal, _) ← match state.convMVar? with
+  let (convRhs, convGoal) ← match state.convMVar? with
     | .some mvar => pure mvar
     | .none => return .invalidAction "Not in conv state"
   let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do

README.md

@@ -90,10 +90,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
-  
-  One particular option for interest for machine learning researchers is the automatic mode.
-  `options.set { "automaticMode": true }`. This makes Pantograph act like
-  LeanDojo, with no resumption necessary to manage your goals.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol