From 9b3eef35ec40a09bba7140ecfc04dafddbd92c27 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 22:22:19 -0700 Subject: [PATCH] fix: Forgot to include the current goals in resume --- Repl.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Repl.lean b/Repl.lean index da594e3..08533b0 100644 --- a/Repl.lean +++ b/Repl.lean @@ -143,12 +143,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .ok (.success nextGoalState) => do let nextGoalState ← match state.options.automaticMode, args.conv? with | true, .none => do - let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" + let .ok result := nextGoalState.resume (nextGoalState.goals ++ 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" + let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" pure result | false, _ => pure nextGoalState let nextStateId := state.nextId