Merge pull request 'doc: Update rationale' (#189) from doc/rationale into dev

Reviewed-on: #189

Pantograph/Delate.lean

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

Pantograph/Goal.lean

@@ -113,14 +113,11 @@ 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]
+@[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 =>
-    let isDuplicate := state.goals.contains goal
-    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
   {
     state with
     savedState := {
@@ -130,19 +127,19 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals. User must ensure `goals` is distinct.
+Brings into scope a list of goals
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
   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.
-  let unassigned := goals.filter λ goal =>
-    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
-    let isDuplicate := state.goals.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
-  return {
+    let unassigned := goals.filter (λ goal =>
+      let mctx := state.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
       state with
       savedState := {
         term := state.savedState.term,

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/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB_MATHLIB:$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,7 +321,9 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+            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.
-- Timeouts for executing tactics is not available. Maybe this will change in the
-  future.
+- Although a timeout feature exists in Pantograph, it relies on the coöperative
+  multitasking from the tactic implementation. There is nothing preventing a
+  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)