From 8857b88d9a0f1b2d8167b18023021366c7b3e530 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Jun 2025 14:52:38 -0700 Subject: [PATCH 1/4] fix(goal): Restore elaboration monad --- Pantograph/Goal.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index d7b170d..9e4bbba 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -507,7 +507,8 @@ protected def GoalState.tryTacticM (state: GoalState) (site : Site) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false) - : Elab.TermElabM TacticResult := + : Elab.TermElabM TacticResult := do + state.restoreElabM withCapturingError do state.step site tacticM guardMVarErrors @@ -567,6 +568,7 @@ protected def GoalState.convEnter (state : GoalState) (site : Site) : let .some goal := state.actingGoal? site | throwNoGoals if let .some (.conv ..) := state.fragments[goal]? then return .invalidAction "Already in conv state" + state.restoreElabM withCapturingError do let (fragments, state') ← state.step' site Fragment.enterConv return { @@ -582,6 +584,7 @@ protected def GoalState.fragmentExit (state : GoalState) (site : Site): let .some goal := state.actingGoal? site | throwNoGoals let .some fragment := state.fragments[goal]? | return .invalidAction "Goal does not have a fragment" + state.restoreElabM withCapturingError do let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments) return { @@ -599,6 +602,7 @@ protected def GoalState.calcEnter (state : GoalState) (site : Site) let .some goal := state.actingGoal? site | throwNoGoals if let .some _ := state.fragments[goal]? then return .invalidAction "Goal already has a fragment" + state.restoreElabM withCapturingError do let fragment := Fragment.enterCalc let fragments := state.fragments.insert goal fragment From dd7c6c36c8e40d29c8bbeea3b51072fab6643746 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Jun 2025 15:00:30 -0700 Subject: [PATCH 2/4] fix(goal): Allow parent expr to be fragments --- Pantograph/Goal.lean | 13 ++++++++++--- Repl.lean | 9 +++++++-- Test/Serial.lean | 2 +- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 9e4bbba..e646448 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -64,7 +64,11 @@ structure GoalState where -- The root goal which is the search target root: MVarId - -- Parent goals assigned to produce this state + /-- + Parent goals which became assigned or fragmented to produce this state. + Note that due to the existence of tactic fragments, parent goals do not + necessarily have an expression assignment. + -/ parentMVars : List MVarId := [] -- Any goal associated with a fragment has a partial tactic which has not @@ -202,8 +206,11 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr @[export pantograph_goal_state_parent_exprs] -protected def GoalState.parentExprs (state : GoalState) : List Expr := - state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get! +protected def GoalState.parentExprs (state : GoalState) : List (Except Fragment Expr) := + state.parentMVars.map λ goal => match state.getMVarEAssignment goal with + | .some e => .ok e + -- A parent goal which is not assigned must have a fragment + | .none => .error state.fragments[goal]! @[always_inline] protected def GoalState.hasUniqueParent (state : GoalState) : Bool := state.parentMVars.length == 1 diff --git a/Repl.lean b/Repl.lean index 3811f96..963503b 100644 --- a/Repl.lean +++ b/Repl.lean @@ -147,10 +147,15 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := match nextGoalState? with | .error error => Protocol.throw error | .ok (.success nextGoalState messages) => do + let env ← getEnv let nextStateId ← newGoalState nextGoalState let parentExprs := nextGoalState.parentExprs - let hasSorry := parentExprs.any (·.hasSorry) - let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·) + let hasSorry := parentExprs.any λ + | .ok e => e.hasSorry + | .error _ => false + let hasUnsafe := parentExprs.any λ + | .ok e => env.hasUnsafe e + | .error _ => false let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run' return { nextStateId? := .some nextStateId, diff --git a/Test/Serial.lean b/Test/Serial.lean index cca7dbd..05dc4af 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -84,7 +84,7 @@ def test_pickling_env_extensions : TestM Unit := do let goal := state.goals[0]! let type ← goal.withContext do let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable! - pure type + instantiateMVars type let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable! let parentExpr := state1.parentExpr! checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma) From 3fab7e7818ca838c5b767b1194709aae3e702d2a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Jun 2025 15:08:46 -0700 Subject: [PATCH 3/4] fix(repl): Allow .none in parentExpr --- Pantograph/Library.lean | 5 +++-- Pantograph/Protocol.lean | 2 +- Test/Integration.lean | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index d8965fc..f361046 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -132,8 +132,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo pure .none let parentExprs? ← if parentExprs then .some <$> state.parentMVars.mapM λ parent => parent.withContext do - let val := state.getMVarEAssignment parent |>.get! - serializeExpression options (← instantiateAll val) + let val? := state.getMVarEAssignment parent + val?.mapM λ val => do + serializeExpression options (← instantiateAll val) else pure .none let goals ← if goals then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 4c02f4d..f83d0ed 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -325,7 +325,7 @@ structure GoalPrintResult where -- The root expression root?: Option Expression := .none -- The filling expression of the parent goal - parentExprs?: Option (List Expression) := .none + parentExprs?: Option (List (Option Expression)) := .none goals: Array Goal := #[] extraMVars: Array Expression := #[] diff --git a/Test/Integration.lean b/Test/Integration.lean index 4db618d..528c9a0 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -91,7 +91,7 @@ def test_tactic : Test := do step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint) ({ root? := .some { pp? := "fun x => ?m.11"}, - parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }], + parentExprs? := .some [.some { pp? := .some "fun x => ?m.11" }], }: Protocol.GoalPrintResult) step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic) ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult) From 16474b2ce84c620f0bae9694c3af0db16d0ba720 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Jun 2025 15:27:51 -0700 Subject: [PATCH 4/4] test(repl): Add test for conv and calc --- Test/Integration.lean | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/Test/Integration.lean b/Test/Integration.lean index 528c9a0..b4e7aba 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -164,6 +164,48 @@ def test_automatic_mode (automatic: Bool): Test := do step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic) ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult) +def test_conv_calc : Test := do + step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet) + ({}: Protocol.OptionsSetResult) + step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart) + ({ stateId := 0, root := "_uniq.163" }: Protocol.GoalStartResult) + let vars := #[ + { name := "_uniq.164", userName := "a", type? := .some { pp? := .some "Nat" }}, + { name := "_uniq.167", userName := "b", type? := .some { pp? := .some "Nat" }}, + { name := "_uniq.170", userName := "h", type? := .some { pp? := .some "b = 2" }}, + ] + let goal : Protocol.Goal := { + vars, + name := "_uniq.171", + target := { pp? := "1 + a + 1 = a + b" }, + } + step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic) + ({ nextStateId? := .some 1, goals? := #[goal], }: Protocol.GoalTacticResult) + step "goal.tactic" ({ stateId := 1, mode? := .some "calc" }: Protocol.GoalTactic) + ({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult) + let goalCalc : Protocol.Goal := { + vars, + name := "_uniq.363", + userName? := .some "calc", + target := { pp? := "1 + a + 1 = a + 1 + 1" }, + } + let goalMain : Protocol.Goal := { + vars, + name := "_uniq.382", + fragment := .calc, + target := { pp? := "a + 1 + 1 = a + b" }, + } + step "goal.tactic" ({ stateId := 2, tactic? := .some "1 + a + 1 = a + 1 + 1" }: Protocol.GoalTactic) + ({ nextStateId? := .some 3, goals? := #[goalCalc, goalMain], }: Protocol.GoalTacticResult) + let goalConv : Protocol.Goal := { + goalCalc with + fragment := .conv, + userName? := .none, + name := "_uniq.450", + } + step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic) + ({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult) + def test_env_add_inspect : Test := do let name1 := "Pantograph.mystery" let name2 := "Pantograph.mystery2" @@ -343,6 +385,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := ("Tactic Timeout", test_tactic_timeout), ("Manual Mode", test_automatic_mode false), ("Automatic Mode", test_automatic_mode true), + ("Conv-Calc", test_conv_calc), ("env.add env.inspect", test_env_add_inspect), ("frontend.process invocation", test_frontend_process), ("frontend.process sorry", test_frontend_process_sorry),