fix(goal): Use `immediateResume` to handle goal

Pantograph/Delate.lean

@@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
   self e := instantiateDelayedMVars e
 
 /--
-Convert an expression to an equivalent form with
+Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas or matchers
 3. No assigned mvars

Pantograph/Goal.lean

@@ -113,11 +113,14 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
   }
 
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume_parent]
+@[export pantograph_goal_state_immediate_resume]
 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
+  let parentGoals := parent.goals.filter λ goal =>
+    let isDuplicate := state.goals.contains goal
+    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
   {
     state with
     savedState := {
@@ -127,25 +130,25 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals
+Brings into scope a list of goals. User must ensure `goals` is distinct.
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
     let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
-  else
+  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+  let unassigned := goals.filter λ goal =>
-    let unassigned := goals.filter (λ goal =>
+    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
-      let mctx := state.mctx
+    let isDuplicate := state.goals.contains goal
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    (¬ isDuplicate) && (¬ isSolved)
-    .ok {
+  return {
-      state with
+    state with
-      savedState := {
+    savedState := {
-        term := state.savedState.term,
+      term := state.savedState.term,
-        tactic := { goals := unassigned },
+      tactic := { goals := unassigned },
-      },
+    },
-    }
+  }
 /--
 Brings into scope all goals from `branch`
 -/

README.md

@@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```

Repl.lean

@@ -321,9 +321,7 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
-          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+          pure $ nextGoalState.immediateResume goalState
-            Protocol.throw $ errorIO "Resuming known goals"
-          pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |

doc/rationale.md

@@ -47,12 +47,12 @@ 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.
-- Although a timeout feature exists in Pantograph, it relies on the coöperative
+- Timeouts for executing tactics is not available. Maybe this will change in the
-  multitasking from the tactic implementation. There is nothing preventing a
+  future.
-  buggy tactic from stalling Lean if it does not check for cancellation often.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
   `def mystery : Nat := :=`) due to Lean's parsing system.
 
+
 ## References
 
 * [Pantograph Paper](https://arxiv.org/abs/2410.16429)