aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 1 Packages Projects Releases Wiki Activity

feat(repl): Detection of sorrys

This commit is contained in:
Leni Aniva 2025-05-01 13:37:35 -04:00
parent 8c1cea17e3
commit ad55ea1a27
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Repl.lean
View File

@ -338,11 +338,14 @@ def execute (command: Protocol.Command): MainM Json := do
pure result pure result
| false, _ => pure nextGoalState | false, _ => pure nextGoalState
let nextStateId ← newGoalState nextGoalState let nextStateId ← newGoalState nextGoalState
let parentExpr := nextGoalState.parentExpr?.get!
let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return { return {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,
goals? := .some goals, goals? := .some goals,
messages? := .some messages, messages? := .some messages,
hasSorry := parentExpr.hasSorry,
hasUnsafe := (← getEnv).hasUnsafe parentExpr,
} }
| .ok (.parseError message) => | .ok (.parseError message) =>
return { messages? := .none, parseError? := .some message } return { messages? := .none, parseError? := .some message }

4
Test/Integration.lean
View File

@ -92,7 +92,9 @@ def test_tactic : Test :=
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic) step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
({ messages? := .some #["tactic 'apply' failed, failed to unify\n ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }: ({ messages? := .some #["tactic 'apply' failed, failed to unify\n ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
Protocol.GoalTacticResult) Protocol.GoalTacticResult),
step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
] ]
example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
simp simp