From 73b5b390b0d116740bba09bc2c5f145ec0b39f9a Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:41 +0100 Subject: [PATCH 01/19] Improve `LocalContext` and `LocalInstance` extraction for sorries --- REPL/Main.lean | 8 ++------ REPL/Snapshots.lean | 49 +++++++++++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 25 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index b05583f7..88455968 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op fun ⟨ctx, g, pos, endPos⟩ => do let (goal, proofState) ← match g with | .tactic g => do - let lctx ← ctx.runMetaM {} do - match ctx.mctx.findDecl? g with - | some decl => return decl.lctx - | none => throwError "unknown metavariable '{g}'" - let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals? + let s ← ProofSnapshot.create ctx none env? [g] rootGoals? pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term lctx (some t) => do let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] @@ -197,7 +193,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do unless (← Meta.isDefEq pft expectedType) do return s!"Error: proof has type {pft} but root goal has type {expectedType}" - let pf ← abstractAllLambdaFVars pf + let pf ← abstractAllLambdaFVars pf >>= instantiateMVars let pft ← Meta.inferType pf >>= instantiateMVars if pf.hasExprMVar then diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index f6936245..e5ddd9a6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·) + /-- Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals. - For convenience, we also allow a list of `Expr`s, and these are appended to the goals as fresh metavariables with the given types. -/ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do - ctx.runMetaM (lctx?.getD {}) do - let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } - pure <| - { coreState := s - coreContext := ← readThe Core.Context - metaState := ← getThe Meta.State - metaContext := ← readThe Meta.Context - termState := {} - termContext := {} - tacticState := { goals } - tacticContext := { elaborator := .anonymous } - rootGoals := match rootGoals? with - | none => goals - | some gs => gs } + -- Get the local context from the goals if not provided. + let lctx ← match lctx? with + | none => match goals with + | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx + | [] => match rootGoals? with + | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx + | _ => pure {} + | some lctx => pure lctx + + ctx.runMetaM lctx do + -- update local instances, which is necessary when `types` is non-empty + Meta.withLocalInstances (lctx.decls.toList.filterMap id) do + let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) + let s ← getThe Core.State + let s := match env? with + | none => s + | some env => { s with env } + pure <| + { coreState := s + coreContext := ← readThe Core.Context + metaState := ← getThe Meta.State + metaContext := ← readThe Meta.Context + termState := {} + termContext := {} + tacticState := { goals } + tacticContext := { elaborator := .anonymous } + rootGoals := match rootGoals? with + | none => goals + | some gs => gs } open Lean.Core in /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/ From b57b7dacbbc0ab974e692a359b79954f882af190 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:42 +0100 Subject: [PATCH 02/19] Add test --- test/local_instance_proof.expected.out | 62 ++++++++++++++++++++++++++ test/local_instance_proof.in | 21 +++++++++ 2 files changed, 83 insertions(+) create mode 100644 test/local_instance_proof.expected.out create mode 100644 test/local_instance_proof.in diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out new file mode 100644 index 00000000..5a93d082 --- /dev/null +++ b/test/local_instance_proof.expected.out @@ -0,0 +1,62 @@ +{"env": 0} + +{"env": 1} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 42}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 47}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"sorries": + [{"proofState": 2, + "pos": {"line": 1, "column": 45}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 50}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 3} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"env": 4} + +{"sorries": + [{"proofState": 4, + "pos": {"line": 1, "column": 17}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 22}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 5} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + +{"sorries": + [{"proofState": 6, + "pos": {"line": 1, "column": 20}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 25}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 6} + +{"proofStatus": "Completed", "proofState": 7, "goals": []} + diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in new file mode 100644 index 00000000..eeefd5ef --- /dev/null +++ b/test/local_instance_proof.in @@ -0,0 +1,21 @@ +{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 2} + +{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0} + +{"cmd": "def test2 : α := sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 4} + +{"cmd": "def test2 : α := by sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 6} From b28f3b78a886c98a4ea55ac7e217cd29beebe792 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:12 +0200 Subject: [PATCH 03/19] First attempt at doing incremental processing of commands --- REPL/Frontend.lean | 60 +++++++++++++++--------- REPL/JSON.lean | 2 +- REPL/Main.lean | 71 +++++++++++++++++++---------- test/pattern_match.expected.out | 6 +++ test/pattern_match.in | 6 +++ test/self_proof_check2.expected.out | 0 test/self_proof_check2.in | 6 +++ 7 files changed, 106 insertions(+), 45 deletions(-) create mode 100644 test/pattern_match.expected.out create mode 100644 test/pattern_match.in create mode 100644 test/self_proof_check2.expected.out create mode 100644 test/self_proof_check2.in diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 81575ed3..54ceeb25 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -9,6 +9,31 @@ open Lean Elab namespace Lean.Elab.IO +partial def filterRootTactics (tree : InfoTree) : Bool := + match tree with + | InfoTree.hole _ => true + | InfoTree.context _ t => filterRootTactics t + | InfoTree.node i _ => match i with + | .ofTacticInfo _ => false + | _ => true + +/-- Traverses a command snapshot tree, yielding each intermediate state. -/ +partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot) +(prevCmdState : Command.State) : + IO (List ((List InfoTree) × Command.State)) := do + let tree := Language.toSnapshotTree snap + let snapshots := tree.getAll + let infotrees := snapshots.map (·.infoTree?) + let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics + let results := [(infotrees, snap.resultSnap.task.get.cmdState)] + -- let results := [(infotrees, prevCmdState)] + match snap.nextCmdSnap? with + | none => return results + | some nextSnapTask => + let nextSnap := nextSnapTask.task.get + let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState + return results ++ nextResults + /-- Wrapper for `IO.processCommands` that enables info states, and returns * the new command state @@ -17,41 +42,34 @@ Wrapper for `IO.processCommands` that enables info states, and returns -/ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) - (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do + (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do let commandState := { commandState with infoState.enabled := true } - let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState - pure (s, s.messages.toList, s.infoState.trees.toList) + let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none + let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState + let s := incs.commandState + pure (s, s.messages.toList, infoTrees) /-- Process some text input, with or without an existing command state. -If there is no existing environment, we parse the input for headers (e.g. import statements), -and create a new environment. -Otherwise, we add to the existing environment. Returns: -1. The header-only command state (only useful when cmdState? is none) -2. The resulting command state after processing the entire input -3. List of messages -4. List of info trees +1. The resulting command state after processing the entire input +2. List of messages +3. List of info trees along with Command.State from the incremental processing -/ def processInput (input : String) (cmdState? : Option Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do + IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName - match cmdState? with + let (parserState, commandState) ← match cmdState? with | none => do - -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx - let headerOnlyState := Command.mkState env messages opts - let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState - return (headerOnlyState, cmdState, messages, trees) - - | some cmdStateBefore => do - let parserState : Parser.ModuleParserState := {} - let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore - return (cmdStateBefore, cmdStateAfter, messages, trees) + pure (parserState, (Command.mkState env messages opts)) + | some cmdState => do + pure ({ : Parser.ModuleParserState }, cmdState) + processCommandsWithInfoTrees inputCtx parserState commandState diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..fa44e2a8 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -47,7 +47,7 @@ deriving ToJson, FromJson structure Pos where line : Nat column : Nat -deriving ToJson, FromJson +deriving ToJson, FromJson, BEq, Hashable /-- Severity of a message. -/ inductive Severity diff --git a/REPL/Main.lean b/REPL/Main.lean index 88455968..3377ae3b 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -111,29 +111,53 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goal pos endPos proofStateId +-- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +-- : M m (List Sorry) := do +-- -- Create a hash set to track positions we've already seen +-- let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {} +-- let mut result : List Sorry := [] + +-- for (trees, cmdState) in treeList do +-- let newSorries ← sorries trees cmdState.env rootGoals? + +-- -- Add only sorries at positions we haven't seen yet +-- for sorr in newSorries do +-- let pos := (sorr.pos, sorr.endPos) +-- unless seenPositions.contains pos do +-- seenPositions := seenPositions.insert pos +-- result := sorr :: result + +-- return result + +def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +: M m (List Sorry) := + treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals? + def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try Lean.PrettyPrinter.ppTactic ⟨stx⟩ catch _ => pure "" -def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) := - trees.flatMap InfoTree.tactics |>.mapM - fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let tactic := Format.pretty (← ppTactic ctx stx) - let proofStateId ← proofState.mapM recordProofSnapshot - return Tactic.of goals tactic pos endPos proofStateId ns - -def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do - trees.flatMap InfoTree.rootGoals |>.mapM - fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none env? goals goals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId - +def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) := + treeList.flatMapM fun (trees, cmdState) => do + trees.flatMap InfoTree.tactics |>.mapM + fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do + let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let tactic := Format.pretty (← ppTactic ctx stx) + let proofStateId ← proofState.mapM recordProofSnapshot + return Tactic.of goals tactic pos endPos proofStateId ns + +def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State)) +: M m (List Sorry) := do + treeList.flatMapM fun (trees, cmdState) => do + trees.flatMap InfoTree.rootGoals |>.mapM + fun ⟨ctx, goals, pos⟩ => do + let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let proofStateId ← proofState.mapM recordProofSnapshot + return Sorry.of goals pos pos proofStateId private def collectFVarsAux : Expr → NameSet | .fvar fvarId => NameSet.empty.insert fvarId.name @@ -298,19 +322,17 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (initialCmdState, cmdState, messages, trees) ← try + let (cmdState, messages, trees) ← try IO.processInput s.cmd initialCmdState? catch ex => return .inr ⟨ex.toString⟩ let messages ← messages.mapM fun m => Message.of m - -- For debugging purposes, sometimes we print out the trees here: - -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees initialCmdState.env none + let sorries ← sorries2 trees none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics trees initialCmdState.env + | some true => tactics trees | _ => pure [] let cmdSnapshot := { cmdState @@ -320,6 +342,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do snap? := none, cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot + let trees := (trees.map (·.1)).flatten + -- For debugging purposes, sometimes we print out the trees here: + -- trees.forM fun t => do IO.println (← t.format) let jsonTrees := match s.infotree with | some "full" => trees | some "tactics" => trees.flatMap InfoTree.retainTacticInfo diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out new file mode 100644 index 00000000..2c1d028e --- /dev/null +++ b/test/pattern_match.expected.out @@ -0,0 +1,6 @@ +{"cmd": "#eval 1 + 1"} + +{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} + +{"tactic": "simp", "proofState": 0} + diff --git a/test/pattern_match.in b/test/pattern_match.in new file mode 100644 index 00000000..2c1d028e --- /dev/null +++ b/test/pattern_match.in @@ -0,0 +1,6 @@ +{"cmd": "#eval 1 + 1"} + +{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} + +{"tactic": "simp", "proofState": 0} + diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out new file mode 100644 index 00000000..e69de29b diff --git a/test/self_proof_check2.in b/test/self_proof_check2.in new file mode 100644 index 00000000..78c0b6a9 --- /dev/null +++ b/test/self_proof_check2.in @@ -0,0 +1,6 @@ +{"cmd": "theorem x : False := sorry\nexample : False := by exact?"} + +{"cmd": "theorem x : False := sorry\nexample : False := sorry"} + +{"proofState": 2, "tactic": "exact?"} + From f402fd8878e834c95150e1bcd6c896ade126625c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 04/19] Implement incrmental collection of sorries --- REPL/Frontend.lean | 83 +++++++++++++++++++++++++--------------------- REPL/Main.lean | 63 +++++++++++++++++------------------ 2 files changed, 76 insertions(+), 70 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 54ceeb25..8a7e809c 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -5,34 +5,41 @@ Authors: Scott Morrison -/ import Lean.Elab.Frontend -open Lean Elab +open Lean Elab Language namespace Lean.Elab.IO -partial def filterRootTactics (tree : InfoTree) : Bool := - match tree with - | InfoTree.hole _ => true - | InfoTree.context _ t => filterRootTactics t - | InfoTree.node i _ => match i with - | .ofTacticInfo _ => false - | _ => true - -/-- Traverses a command snapshot tree, yielding each intermediate state. -/ -partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot) -(prevCmdState : Command.State) : - IO (List ((List InfoTree) × Command.State)) := do - let tree := Language.toSnapshotTree snap - let snapshots := tree.getAll - let infotrees := snapshots.map (·.infoTree?) - let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics - let results := [(infotrees, snap.resultSnap.task.get.cmdState)] - -- let results := [(infotrees, prevCmdState)] - match snap.nextCmdSnap? with - | none => return results - | some nextSnapTask => - let nextSnap := nextSnapTask.task.get - let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState - return results ++ nextResults +partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext) + (parserState : Parser.ModuleParserState) (commandState : Command.State) + (old? : Option IncrementalState) : + BaseIO (List (IncrementalState × Option InfoTree)) := do + let task ← Language.Lean.processCommands inputCtx parserState commandState + (old?.map fun old => (old.inputCtx, old.initialSnap)) + return go task.get task #[] +where + go initialSnap t commands := + let snap := t.get + let commands := commands.push snap + -- Opting into reuse also enables incremental reporting, so make sure to collect messages from + -- all snapshots + let messages := toSnapshotTree initialSnap + |>.getAll.map (·.diagnostics.msgLog) + |>.foldl (· ++ ·) {} + -- In contrast to messages, we should collect info trees only from the top-level command + -- snapshots as they subsume any info trees reported incrementally by their children. + let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let result : (IncrementalState × Option InfoTree) := + ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees } + , parserState := snap.parserState + , cmdPos := snap.parserState.pos + , commands := commands.map (·.stx) + , inputCtx := inputCtx + , initialSnap := initialSnap + }, snap.infoTreeSnap.get.infoTree?) + if let some next := snap.nextCmdSnap? then + result :: go initialSnap next.task commands + else + [result] /-- Wrapper for `IO.processCommands` that enables info states, and returns @@ -42,12 +49,11 @@ Wrapper for `IO.processCommands` that enables info states, and returns -/ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) - (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do + (commandState : Command.State) (incrementalState? : Option IncrementalState := none) + : IO (List (IncrementalState × Option InfoTree) × List Message) := do let commandState := { commandState with infoState.enabled := true } - let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none - let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState - let s := incs.commandState - pure (s, s.messages.toList, infoTrees) + let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState? + pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {}) /-- Process some text input, with or without an existing command state. @@ -59,17 +65,20 @@ Returns: -/ def processInput (input : String) (cmdState? : Option Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do + IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName - - let (parserState, commandState) ← match cmdState? with + match cmdState? with | none => do + -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx - pure (parserState, (Command.mkState env messages opts)) - | some cmdState => do - pure ({ : Parser.ModuleParserState }, cmdState) - processCommandsWithInfoTrees inputCtx parserState commandState + let headerOnlyState := Command.mkState env messages opts + let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState + return (headerOnlyState, incStates) + | some cmdStateBefore => do + let parserState : Parser.ModuleParserState := {} + let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore + return (cmdStateBefore, incStates) diff --git a/REPL/Main.lean b/REPL/Main.lean index 3377ae3b..449eabd4 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -111,27 +111,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goal pos endPos proofStateId --- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) --- : M m (List Sorry) := do --- -- Create a hash set to track positions we've already seen --- let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {} --- let mut result : List Sorry := [] - --- for (trees, cmdState) in treeList do --- let newSorries ← sorries trees cmdState.env rootGoals? - --- -- Add only sorries at positions we haven't seen yet --- for sorr in newSorries do --- let pos := (sorr.pos, sorr.endPos) --- unless seenPositions.contains pos do --- seenPositions := seenPositions.insert pos --- result := sorr :: result - --- return result - -def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) +(rootGoals? : Option (List MVarId)) : M m (List Sorry) := - treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals? + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let s ← sorries infoTree?.toList prevEnv rootGoals? + let restSorries ← sorriesCmd rest state.commandState.env rootGoals? + return s ++ restSorries def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try @@ -139,22 +127,22 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := catch _ => pure "" -def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) := - treeList.flatMapM fun (trees, cmdState) => do - trees.flatMap InfoTree.tactics |>.mapM +def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) := + treeList.flatMapM fun (state, infoTree?) => do + infoTree?.toList.flatMap InfoTree.tactics |>.mapM fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals) + let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals) let goals := s!"{(← ctx.ppGoals goals)}".trim let tactic := Format.pretty (← ppTactic ctx stx) let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns -def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State)) +def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree)) : M m (List Sorry) := do - treeList.flatMapM fun (trees, cmdState) => do - trees.flatMap InfoTree.rootGoals |>.mapM + treeList.flatMapM fun (state, infoTree?) => do + infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals) + let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals) let goals := s!"{(← ctx.ppGoals goals)}".trim let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goals pos pos proofStateId @@ -322,17 +310,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (cmdState, messages, trees) ← try + let (initialCmdState, incStates, messages) ← try IO.processInput s.cmd initialCmdState? catch ex => return .inr ⟨ex.toString⟩ + + let mut prevPos := 0 + for (incState, _) in incStates do + let endPos := incState.cmdPos + let processedText := incState.inputCtx.input.extract prevPos endPos + IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}" + prevPos := endPos + + let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m - let sorries ← sorries2 trees none + let sorries ← sorriesCmd incStates initialCmdState.env none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics trees + | some true => tactics incStates | _ => pure [] let cmdSnapshot := { cmdState @@ -342,7 +339,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do snap? := none, cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot - let trees := (trees.map (·.1)).flatten + let trees := cmdState.infoState.trees.toList -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) let jsonTrees := match s.infotree with From e252f5758d14396e1b72f417304643cc60a545bc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 05/19] Fix test output --- test/self_proof_check2.expected.out | 49 +++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out index e69de29b..99d5339f 100644 --- a/test/self_proof_check2.expected.out +++ b/test/self_proof_check2.expected.out @@ -0,0 +1,49 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "info", + "pos": {"line": 2, "column": 22}, + "endPos": {"line": 2, "column": 28}, + "data": "Try this: exact x"}, + {"severity": "info", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 28}, + "data": "Goals accomplished!"}], + "env": 0} + +{"sorries": + [{"proofState": 1, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}, + {"proofState": 2, + "pos": {"line": 2, "column": 19}, + "goal": "⊢ False", + "endPos": {"line": 2, "column": 24}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "warning", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": "Completed", + "proofState": 3, + "messages": + [{"severity": "info", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "Try this: exact x"}], + "goals": []} + From 849f8679d94afaeac7922faad487b6e4e23ee906 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 06/19] Update tests --- ...out => in_command_dependency.expected.out} | 6 +--- ...oof_check2.in => in_command_dependency.in} | 0 test/pattern_match.expected.out | 28 +++++++++++++++++-- test/pattern_match.in | 9 ++++-- 4 files changed, 33 insertions(+), 10 deletions(-) rename test/{self_proof_check2.expected.out => in_command_dependency.expected.out} (87%) rename test/{self_proof_check2.in => in_command_dependency.in} (100%) diff --git a/test/self_proof_check2.expected.out b/test/in_command_dependency.expected.out similarity index 87% rename from test/self_proof_check2.expected.out rename to test/in_command_dependency.expected.out index 99d5339f..e3ba5583 100644 --- a/test/self_proof_check2.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,11 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this: exact x"}, - {"severity": "info", - "pos": {"line": 2, "column": 0}, - "endPos": {"line": 2, "column": 28}, - "data": "Goals accomplished!"}], + "data": "Try this: exact x"}], "env": 0} {"sorries": diff --git a/test/self_proof_check2.in b/test/in_command_dependency.in similarity index 100% rename from test/self_proof_check2.in rename to test/in_command_dependency.in diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out index 2c1d028e..2e16d41f 100644 --- a/test/pattern_match.expected.out +++ b/test/pattern_match.expected.out @@ -1,6 +1,28 @@ -{"cmd": "#eval 1 + 1"} +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 77}, + "goal": + "⊢ (fun x =>\n match x with\n | (x, fst, snd) => x = x) =\n fun x => True", + "endPos": {"line": 1, "column": 82}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} -{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": + ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]} -{"tactic": "simp", "proofState": 0} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"proofStatus": "Completed", "proofState": 4, "goals": []} + +{"env": 1} diff --git a/test/pattern_match.in b/test/pattern_match.in index 2c1d028e..a863f0b9 100644 --- a/test/pattern_match.in +++ b/test/pattern_match.in @@ -1,6 +1,11 @@ -{"cmd": "#eval 1 + 1"} +{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"} -{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} +{"tactic": "funext ⟨x, y, z⟩", "proofState": 0} + +{"tactic": "show (x = x) = True", "proofState": 1} + +{"tactic": "rw [eq_self_iff_true]", "proofState": 2} {"tactic": "simp", "proofState": 0} +{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"} From 5b795ed0be04631ee9eb75ae1b49168a55882a86 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:14 +0200 Subject: [PATCH 07/19] Improving fine-grained environment --- REPL/Main.lean | 63 +++++++++++++++++++++++++-------------------- REPL/Snapshots.lean | 33 +++++++++++++++++++----- 2 files changed, 62 insertions(+), 34 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 449eabd4..078c44b5 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -127,25 +127,39 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := catch _ => pure "" -def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) := - treeList.flatMapM fun (state, infoTree?) => do - infoTree?.toList.flatMap InfoTree.tactics |>.mapM - fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let tactic := Format.pretty (← ppTactic ctx stx) - let proofStateId ← proofState.mapM recordProofSnapshot - return Tactic.of goals tactic pos endPos proofStateId ns - -def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree)) -: M m (List Sorry) := do - treeList.flatMapM fun (state, infoTree?) => do - infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM - fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId +def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) := + trees.flatMap InfoTree.tactics |>.mapM + fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do + let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let tactic := Format.pretty (← ppTactic ctx stx) + let proofStateId ← proofState.mapM recordProofSnapshot + return Tactic.of goals tactic pos endPos proofStateId ns + +def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let ts ← tactics infoTree?.toList prevEnv + let restTactics ← tacticsCmd rest state.commandState.env + return ts ++ restTactics + +def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do + trees.flatMap InfoTree.rootGoals |>.mapM + fun ⟨ctx, goals, pos⟩ => do + let proofState := some (← ProofSnapshot.create ctx none env? goals goals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let proofStateId ← proofState.mapM recordProofSnapshot + return Sorry.of goals pos pos proofStateId + +def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : + M m (List Sorry) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv + let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env + return sorries ++ restSorries private def collectFVarsAux : Expr → NameSet | .fvar fvarId => NameSet.empty.insert fvarId.name @@ -315,21 +329,14 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do catch ex => return .inr ⟨ex.toString⟩ - let mut prevPos := 0 - for (incState, _) in incStates do - let endPos := incState.cmdPos - let processedText := incState.inputCtx.input.extract prevPos endPos - IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}" - prevPos := endPos - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics incStates + | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] let cmdSnapshot := { cmdState diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index e5ddd9a6..4fd6cfdb 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -191,7 +191,7 @@ Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, an For convenience, we also allow a list of `Expr`s, and these are appended to the goals as fresh metavariables with the given types. -/ -def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) +def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do -- Get the local context from the goals if not provided. @@ -207,12 +207,33 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi -- update local instances, which is necessary when `types` is non-empty Meta.withLocalInstances (lctx.decls.toList.filterMap id) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } + + -- Create a filtered environment that excludes the new (non-auxiliary) declarations + -- Necessary to avoid self-references in proofs in tactic mode, while still allowing + -- auxiliary declarations to be used in the proof. + let coreState ← match prevEnv? with + | none => getThe Core.State + | some prevEnv => do + let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName) + let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n + + let currentConsts := ctx.env.constants.map₂.toList + let prevConsts := prevEnv.constants.map₂.toList + let diff := currentConsts.filter (fun (name, _) => + !prevConsts.any (fun (name', _) => name == name')) + let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name + + -- Print for debugging purposes + IO.println s!"Constants to filter: {declsToFilter}" + IO.println s!"Replayed constants: {filteredConstants.map (·.1)}" + + let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants) + -- let filteredEnv := prevEnv + let s ← getThe Core.State + pure { s with env := filteredEnv } + pure <| - { coreState := s + { coreState := coreState coreContext := ← readThe Core.Context metaState := ← getThe Meta.State metaContext := ← readThe Meta.Context From 0fcfed993cd9222fdfa7d6dc62ac240f110a7740 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:14 +0200 Subject: [PATCH 08/19] Revert constant replay --- REPL/Snapshots.lean | 31 +++++-------------------------- test/pattern_match.expected.out | 28 ---------------------------- test/pattern_match.in | 11 ----------- 3 files changed, 5 insertions(+), 65 deletions(-) delete mode 100644 test/pattern_match.expected.out delete mode 100644 test/pattern_match.in diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 4fd6cfdb..d87981e6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -207,33 +207,12 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option -- update local instances, which is necessary when `types` is non-empty Meta.withLocalInstances (lctx.decls.toList.filterMap id) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - - -- Create a filtered environment that excludes the new (non-auxiliary) declarations - -- Necessary to avoid self-references in proofs in tactic mode, while still allowing - -- auxiliary declarations to be used in the proof. - let coreState ← match prevEnv? with - | none => getThe Core.State - | some prevEnv => do - let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName) - let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n - - let currentConsts := ctx.env.constants.map₂.toList - let prevConsts := prevEnv.constants.map₂.toList - let diff := currentConsts.filter (fun (name, _) => - !prevConsts.any (fun (name', _) => name == name')) - let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name - - -- Print for debugging purposes - IO.println s!"Constants to filter: {declsToFilter}" - IO.println s!"Replayed constants: {filteredConstants.map (·.1)}" - - let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants) - -- let filteredEnv := prevEnv - let s ← getThe Core.State - pure { s with env := filteredEnv } - + let s ← getThe Core.State + let s := match prevEnv? with + | none => s + | some env => { s with env } pure <| - { coreState := coreState + { coreState := s coreContext := ← readThe Core.Context metaState := ← getThe Meta.State metaContext := ← readThe Meta.Context diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out deleted file mode 100644 index 2e16d41f..00000000 --- a/test/pattern_match.expected.out +++ /dev/null @@ -1,28 +0,0 @@ -{"sorries": - [{"proofState": 0, - "pos": {"line": 1, "column": 77}, - "goal": - "⊢ (fun x =>\n match x with\n | (x, fst, snd) => x = x) =\n fun x => True", - "endPos": {"line": 1, "column": 82}}], - "messages": - [{"severity": "warning", - "pos": {"line": 1, "column": 4}, - "endPos": {"line": 1, "column": 7}, - "data": "declaration uses 'sorry'"}], - "env": 0} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 1, - "goals": - ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 2, - "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]} - -{"proofStatus": "Completed", "proofState": 3, "goals": []} - -{"proofStatus": "Completed", "proofState": 4, "goals": []} - -{"env": 1} - diff --git a/test/pattern_match.in b/test/pattern_match.in deleted file mode 100644 index a863f0b9..00000000 --- a/test/pattern_match.in +++ /dev/null @@ -1,11 +0,0 @@ -{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"} - -{"tactic": "funext ⟨x, y, z⟩", "proofState": 0} - -{"tactic": "show (x = x) = True", "proofState": 1} - -{"tactic": "rw [eq_self_iff_true]", "proofState": 2} - -{"tactic": "simp", "proofState": 0} - -{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"} From f33a50eb214cb9325641cbb83591f1b4ea2e97cc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:15 +0200 Subject: [PATCH 09/19] Fix v4.22.0-rc2 --- REPL/Frontend.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 8a7e809c..bc2dff1e 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -27,15 +27,15 @@ where |>.foldl (· ++ ·) {} -- In contrast to messages, we should collect info trees only from the top-level command -- snapshots as they subsume any info trees reported incrementally by their children. - let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' let result : (IncrementalState × Option InfoTree) := - ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees } + ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees } , parserState := snap.parserState , cmdPos := snap.parserState.pos , commands := commands.map (·.stx) , inputCtx := inputCtx , initialSnap := initialSnap - }, snap.infoTreeSnap.get.infoTree?) + }, snap.elabSnap.infoTreeSnap.get.infoTree?) if let some next := snap.nextCmdSnap? then result :: go initialSnap next.task commands else From 98d737c2c0cb1c4e1a035593d72778d7ca5e5115 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:24 +0200 Subject: [PATCH 10/19] Fix test v4.24.0-rc1 --- test/in_command_dependency.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out index e3ba5583..66371d34 100644 --- a/test/in_command_dependency.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,7 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this: exact x"}], + "data": "Try this:\n exact x"}], "env": 0} {"sorries": @@ -40,6 +40,6 @@ [{"severity": "info", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "Try this: exact x"}], + "data": "Try this:\n exact x"}], "goals": []} From 4d97344f3e2571a541e2f95dd01147b5f0ccec87 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Wed, 22 Oct 2025 11:48:02 +0200 Subject: [PATCH 11/19] Fix test v4.25.0-rc1 --- test/in_command_dependency.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out index 66371d34..e22d70ba 100644 --- a/test/in_command_dependency.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,7 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this:\n exact x"}], + "data": "Try this:\n [apply] exact x"}], "env": 0} {"sorries": @@ -40,6 +40,6 @@ [{"severity": "info", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "Try this:\n exact x"}], + "data": "Try this:\n [apply] exact x"}], "goals": []} From 5bc2e03f4720b8b061d4df639bef730d20dc2f20 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:45 +0200 Subject: [PATCH 12/19] Init commit --- REPL/Frontend.lean | 5 ++- REPL/Main.lean | 97 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 98 insertions(+), 4 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index bc2dff1e..4e79fa6b 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -64,6 +64,7 @@ Returns: 3. List of info trees along with Command.State from the incremental processing -/ def processInput (input : String) (cmdState? : Option Command.State) + (incrementalState? : Option IncrementalState := none) (opts : Options := {}) (fileName : Option String := none) : IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do Lean.initSearchPath (← Lean.findSysroot) @@ -76,9 +77,9 @@ def processInput (input : String) (cmdState? : Option Command.State) let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx let headerOnlyState := Command.mkState env messages opts - let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState + let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? return (headerOnlyState, incStates) | some cmdStateBefore => do let parserState : Parser.ModuleParserState := {} - let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore + let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? return (cmdStateBefore, incStates) diff --git a/REPL/Main.lean b/REPL/Main.lean index 078c44b5..08f04416 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -72,7 +72,17 @@ structure State where and report the numerical index for the recorded state at each sorry. -/ proofStates : Array ProofSnapshot := #[] - + /-- + Stores the command text and incremental states for each command, indexed by command ID. + Used for prefix matching to enable incremental processing reuse. + -/ + cmdTexts : Array String := #[] + cmdIncrementalStates : Array (List (IncrementalState × Option InfoTree)) := #[] + /-- + Stores the environment ID that each command was built upon. + Used to ensure prefix matching only considers compatible environment chains. + -/ + cmdEnvChain : Array (Option Nat) := #[] /-- The Lean REPL monad. @@ -88,12 +98,80 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do modify fun s => { s with cmdStates := s.cmdStates.push state } return id +/-- Record command text and incremental states for prefix matching reuse. -/ +def recordCommandIncrementals (cmdText : String) + (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do + modify fun s => { s with + cmdTexts := s.cmdTexts.push cmdText + cmdIncrementalStates := s.cmdIncrementalStates.push incStates + cmdEnvChain := s.cmdEnvChain.push envId? } + /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do let id := (← get).proofStates.size modify fun s => { s with proofStates := s.proofStates.push proofState } return id +/-- Find the longest common prefix between two strings. -/ +def longestCommonPrefix (s1 s2 : String) : Nat := + let chars1 := s1.toList + let chars2 := s2.toList + let rec loop (acc : Nat) : List Char → List Char → Nat + | [], _ => acc + | _, [] => acc + | c1 :: cs1, c2 :: cs2 => + if c1 = c2 then loop (acc + 1) cs1 cs2 else acc + loop 0 chars1 chars2 + +/-- Check if two commands start from the exact same base environment. -/ +def haveSameBaseEnv (envId1? envId2? : Option Nat) : Bool := + match envId1?, envId2? with + | none, none => true -- Both are from fresh environments + | some id1, some id2 => id1 = id2 -- Same environment ID + | _, _ => false -- One fresh, one inherited - different base environments + +/-- Find the best incremental state to reuse based on longest prefix matching from commands with the same base environment. -/ +def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do + let state ← get + if state.cmdTexts.isEmpty then + return none + + -- Find the command with the longest common prefix in the same environment chain + let mut bestPrefix := 0 + let mut bestIncrState : Option IncrementalState := none + + for i in [:state.cmdTexts.size] do + -- Check if this command starts from the same base environment + let cmdEnvId := if i < state.cmdEnvChain.size then state.cmdEnvChain[i]! else none + let hasSameBase := haveSameBaseEnv envId? cmdEnvId + + if hasSameBase then + let cmdText := state.cmdTexts[i]! + let prefixLen := longestCommonPrefix newCmd cmdText + + -- Only consider significant prefixes (at least 10 characters to avoid noise) + if prefixLen > bestPrefix && prefixLen ≥ 10 then + let incStates := state.cmdIncrementalStates[i]! + -- Find the latest incremental state that doesn't exceed our prefix + for (incState, _) in incStates.reverse do + -- Convert string prefix length to byte position for comparison + let prefixBytes := (cmdText.take prefixLen).utf8ByteSize + if incState.cmdPos.byteIdx ≤ prefixBytes then + bestPrefix := prefixLen + bestIncrState := some incState + break + + -- Print debug information about reuse + match bestIncrState with + | some _ => IO.println s!"Found incremental state to reuse (prefix length: {bestPrefix}, env chain compatible)" + | none => + if state.cmdTexts.isEmpty then + IO.println "No previous commands available for reuse" + else + IO.println "No suitable incremental state found for reuse (considering environment chain compatibility)" + + return bestIncrState + def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with @@ -324,11 +402,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState + + -- Find the best incremental state to reuse based on prefix matching + let bestIncrementalState? ← findBestIncrementalState s.cmd s.env + let (initialCmdState, incStates, messages) ← try - IO.processInput s.cmd initialCmdState? + IO.processInput s.cmd initialCmdState? (incrementalState? := bestIncrementalState?) catch ex => return .inr ⟨ex.toString⟩ + -- Store the command text and incremental states for future reuse + recordCommandIncrementals s.cmd incStates s.env + + -- showcase the input string for each incremental state + let mut prevPos := 0 + for (incState, _) in incStates do + let endPos := incState.cmdPos + let processedText := incState.inputCtx.input.extract prevPos endPos + IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n```lean4\n{processedText}\n```" + prevPos := endPos + let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From dc47b431fc48958cd186233b2d4c4eea479b69b6 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 13/19] Implement trie-based prefix matching --- REPL/Frontend.lean | 28 +++++++---- REPL/Main.lean | 115 +++++++++++++++------------------------------ 2 files changed, 57 insertions(+), 86 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 4e79fa6b..e549a1fa 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import Lean.Elab.Frontend +import Std.Data.HashMap open Lean Elab Language @@ -57,29 +58,40 @@ def processCommandsWithInfoTrees /-- Process some text input, with or without an existing command state. +Supports header caching to avoid reprocessing the same imports repeatedly. Returns: 1. The resulting command state after processing the entire input 2. List of messages 3. List of info trees along with Command.State from the incremental processing +4. Updated header cache mapping import keys to Command.State -/ def processInput (input : String) (cmdState? : Option Command.State) (incrementalState? : Option IncrementalState := none) + (headerCache : Std.HashMap String Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do + IO (Command.State × List (IncrementalState × Option InfoTree) × List Message × (Std.HashMap String Command.State)) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName match cmdState? with | none => do - -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← processHeader header opts messages inputCtx - let headerOnlyState := Command.mkState env messages opts - let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? - return (headerOnlyState, incStates) + let importKey := (input.take parserState.pos.byteIdx).trim + match headerCache.get? importKey with + | some cachedHeaderState => do + -- Header is cached, use it as the base command state + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cachedHeaderState incrementalState? + return (cachedHeaderState, incStates, messages, headerCache) + | none => do + -- Header not cached, process it and cache the result + let (env, messages) ← processHeader header opts messages inputCtx + let headerOnlyState := Command.mkState env messages opts + let headerCache := headerCache.insert importKey headerOnlyState + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? + return (headerOnlyState, incStates, messages, headerCache) | some cmdStateBefore => do let parserState : Parser.ModuleParserState := {} - let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? - return (cmdStateBefore, incStates) + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? + return (cmdStateBefore, incStates, messages, headerCache) diff --git a/REPL/Main.lean b/REPL/Main.lean index 08f04416..523269fa 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,8 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import Lean.Data.Trie +import Std.Data.HashMap /-! # A REPL for Lean. @@ -73,16 +75,16 @@ structure State where -/ proofStates : Array ProofSnapshot := #[] /-- - Stores the command text and incremental states for each command, indexed by command ID. - Used for prefix matching to enable incremental processing reuse. + Trie-based storage for fast prefix matching, organized by environment ID. + Map from environment ID (None for fresh env) to trie of command prefixes with incremental states. -/ - cmdTexts : Array String := #[] - cmdIncrementalStates : Array (List (IncrementalState × Option InfoTree)) := #[] + envTries : Std.HashMap (Option Nat) (Lean.Data.Trie IncrementalState) := Std.HashMap.emptyWithCapacity 8 /-- - Stores the environment ID that each command was built upon. - Used to ensure prefix matching only considers compatible environment chains. + Cache for processed headers (import statements) to avoid reprocessing the same imports repeatedly. + Maps import raw string to the processed command state. -/ - cmdEnvChain : Array (Option Nat) := #[] + headerCache : Std.HashMap String Command.State := Std.HashMap.emptyWithCapacity 8 + /-- The Lean REPL monad. @@ -98,13 +100,24 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do modify fun s => { s with cmdStates := s.cmdStates.push state } return id +/-- Add all incremental states of a command to the trie at their corresponding prefix positions -/ +def addCommandToTrie (cmdText : String) + (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do + let state ← get + let currentTrie := state.envTries.get? envId? |>.getD Lean.Data.Trie.empty + + let mut newTrie := currentTrie + for (incState, _) in incStates do + let prefixPos := incState.cmdPos.byteIdx + let cmdPrefix : String := (cmdText.take prefixPos).trim + newTrie := newTrie.insert cmdPrefix incState + + modify fun s => { s with envTries := s.envTries.insert envId? newTrie } + /-- Record command text and incremental states for prefix matching reuse. -/ def recordCommandIncrementals (cmdText : String) (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do - modify fun s => { s with - cmdTexts := s.cmdTexts.push cmdText - cmdIncrementalStates := s.cmdIncrementalStates.push incStates - cmdEnvChain := s.cmdEnvChain.push envId? } + addCommandToTrie cmdText incStates envId? /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do @@ -112,65 +125,17 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do modify fun s => { s with proofStates := s.proofStates.push proofState } return id -/-- Find the longest common prefix between two strings. -/ -def longestCommonPrefix (s1 s2 : String) : Nat := - let chars1 := s1.toList - let chars2 := s2.toList - let rec loop (acc : Nat) : List Char → List Char → Nat - | [], _ => acc - | _, [] => acc - | c1 :: cs1, c2 :: cs2 => - if c1 = c2 then loop (acc + 1) cs1 cs2 else acc - loop 0 chars1 chars2 - -/-- Check if two commands start from the exact same base environment. -/ -def haveSameBaseEnv (envId1? envId2? : Option Nat) : Bool := - match envId1?, envId2? with - | none, none => true -- Both are from fresh environments - | some id1, some id2 => id1 = id2 -- Same environment ID - | _, _ => false -- One fresh, one inherited - different base environments - -/-- Find the best incremental state to reuse based on longest prefix matching from commands with the same base environment. -/ +/-- Find the best incremental state using trie-based prefix matching -/ def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do let state ← get - if state.cmdTexts.isEmpty then - return none - - -- Find the command with the longest common prefix in the same environment chain - let mut bestPrefix := 0 - let mut bestIncrState : Option IncrementalState := none - - for i in [:state.cmdTexts.size] do - -- Check if this command starts from the same base environment - let cmdEnvId := if i < state.cmdEnvChain.size then state.cmdEnvChain[i]! else none - let hasSameBase := haveSameBaseEnv envId? cmdEnvId - - if hasSameBase then - let cmdText := state.cmdTexts[i]! - let prefixLen := longestCommonPrefix newCmd cmdText - - -- Only consider significant prefixes (at least 10 characters to avoid noise) - if prefixLen > bestPrefix && prefixLen ≥ 10 then - let incStates := state.cmdIncrementalStates[i]! - -- Find the latest incremental state that doesn't exceed our prefix - for (incState, _) in incStates.reverse do - -- Convert string prefix length to byte position for comparison - let prefixBytes := (cmdText.take prefixLen).utf8ByteSize - if incState.cmdPos.byteIdx ≤ prefixBytes then - bestPrefix := prefixLen - bestIncrState := some incState - break - - -- Print debug information about reuse - match bestIncrState with - | some _ => IO.println s!"Found incremental state to reuse (prefix length: {bestPrefix}, env chain compatible)" - | none => - if state.cmdTexts.isEmpty then - IO.println "No previous commands available for reuse" - else - IO.println "No suitable incremental state found for reuse (considering environment chain compatibility)" - - return bestIncrState + let trimmedCmd := newCmd.trim + let trie? := state.envTries.get? envId? + match trie? with + | none => return none + | some trie => + match trie.matchPrefix trimmedCmd 0 with + | some incState => return some incState + | none => return none def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := @@ -406,22 +371,16 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do -- Find the best incremental state to reuse based on prefix matching let bestIncrementalState? ← findBestIncrementalState s.cmd s.env - let (initialCmdState, incStates, messages) ← try - IO.processInput s.cmd initialCmdState? (incrementalState? := bestIncrementalState?) + let (initialCmdState, incStates, messages, headerCache) ← try + IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache catch ex => return .inr ⟨ex.toString⟩ + modify fun st => { st with headerCache := headerCache } + -- Store the command text and incremental states for future reuse recordCommandIncrementals s.cmd incStates s.env - -- showcase the input string for each incremental state - let mut prevPos := 0 - for (incState, _) in incStates do - let endPos := incState.cmdPos - let processedText := incState.inputCtx.input.extract prevPos endPos - IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n```lean4\n{processedText}\n```" - prevPos := endPos - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From b6629a2ef0d3743508330aa656d29c7a9482ef11 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 14/19] Add test example --- test/Mathlib/test/incrementality.expected.out | 68 +++++++++++++++++++ test/Mathlib/test/incrementality.in | 3 + 2 files changed, 71 insertions(+) create mode 100644 test/Mathlib/test/incrementality.expected.out create mode 100644 test/Mathlib/test/incrementality.in diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out new file mode 100644 index 00000000..28cbaee6 --- /dev/null +++ b/test/Mathlib/test/incrementality.expected.out @@ -0,0 +1,68 @@ +{"tactics": + [{"usedConstants": + ["Nat.gcd", + "HMul.hMul", + "Mathlib.Meta.NormNum.isNat_eq_true", + "instMulNat", + "instOfNatNat", + "Mathlib.Meta.NormNum.isNat_ofNat", + "Tactic.NormNum.nat_gcd_helper_2", + "Nat.instAddMonoidWithOne", + "Nat", + "Eq.refl", + "Mathlib.Meta.NormNum.instAddMonoidWithOneNat", + "Tactic.NormNum.isNat_gcd", + "OfNat.ofNat", + "instHMul"], + "tactic": "norm_num", + "proofState": 0, + "pos": {"line": 2, "column": 60}, + "goals": "⊢ Nat.gcd 180 168 = 12", + "endPos": {"line": 2, "column": 68}}, + {"usedConstants": ["Eq.refl"], + "tactic": "rfl", + "proofState": 1, + "pos": {"line": 10, "column": 2}, + "goals": "α✝ : Sort u_1\nn : α✝\n⊢ n = n", + "endPos": {"line": 10, "column": 5}}], + "messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 5}, + "data": "9227465"}], + "env": 0} + +{"tactics": + [{"usedConstants": + ["Nat.gcd", + "HMul.hMul", + "Mathlib.Meta.NormNum.isNat_eq_true", + "instMulNat", + "instOfNatNat", + "Mathlib.Meta.NormNum.isNat_ofNat", + "Tactic.NormNum.nat_gcd_helper_2", + "Nat.instAddMonoidWithOne", + "Nat", + "Eq.refl", + "Mathlib.Meta.NormNum.instAddMonoidWithOneNat", + "Tactic.NormNum.isNat_gcd", + "OfNat.ofNat", + "instHMul"], + "tactic": "norm_num", + "proofState": 2, + "pos": {"line": 2, "column": 60}, + "goals": "⊢ Nat.gcd 180 168 = 12", + "endPos": {"line": 2, "column": 68}}, + {"usedConstants": ["Nat", "Eq.refl"], + "tactic": "rfl", + "proofState": 3, + "pos": {"line": 10, "column": 2}, + "goals": "n : ℕ\n⊢ n = n + 0", + "endPos": {"line": 10, "column": 5}}], + "messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 5}, + "data": "9227465"}], + "env": 1} + diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in new file mode 100644 index 00000000..43e5fb5e --- /dev/null +++ b/test/Mathlib/test/incrementality.in @@ -0,0 +1,3 @@ +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} + +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} From 1af83925b5f7f21c76d276bafbddccdcd8a26fc9 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 15/19] Fix sensitivity to comments and whitespaces in the header --- REPL/Frontend.lean | 2 +- test/Mathlib/test/incrementality.expected.out | 2 ++ test/Mathlib/test/incrementality.in | 2 ++ 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index e549a1fa..20885db9 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -78,7 +78,7 @@ def processInput (input : String) (cmdState? : Option Command.State) match cmdState? with | none => do let (header, parserState, messages) ← Parser.parseHeader inputCtx - let importKey := (input.take parserState.pos.byteIdx).trim + let importKey := toString header.raw -- do not contain comments and whitespace match headerCache.get? importKey with | some cachedHeaderState => do -- Header is cached, use it as the base command state diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out index 28cbaee6..db70a9b3 100644 --- a/test/Mathlib/test/incrementality.expected.out +++ b/test/Mathlib/test/incrementality.expected.out @@ -66,3 +66,5 @@ "data": "9227465"}], "env": 1} +{"env": 2} + diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in index 43e5fb5e..19bea50e 100644 --- a/test/Mathlib/test/incrementality.in +++ b/test/Mathlib/test/incrementality.in @@ -1,3 +1,5 @@ {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} + +{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"} From 04b2028d59acc5b77367fb4c68987a380bcafc1b Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 16/19] Fix trie stack overflow issue --- REPL/Main.lean | 5 +- REPL/Util/Trie.lean | 146 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 149 insertions(+), 2 deletions(-) create mode 100644 REPL/Util/Trie.lean diff --git a/REPL/Main.lean b/REPL/Main.lean index 523269fa..fb6a5e70 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,7 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import REPL.Util.Trie import Lean.Data.Trie import Std.Data.HashMap @@ -110,7 +111,7 @@ def addCommandToTrie (cmdText : String) for (incState, _) in incStates do let prefixPos := incState.cmdPos.byteIdx let cmdPrefix : String := (cmdText.take prefixPos).trim - newTrie := newTrie.insert cmdPrefix incState + newTrie := REPL.Util.Trie.insert newTrie cmdPrefix incState modify fun s => { s with envTries := s.envTries.insert envId? newTrie } @@ -133,7 +134,7 @@ def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Opti match trie? with | none => return none | some trie => - match trie.matchPrefix trimmedCmd 0 with + match REPL.Util.Trie.matchPrefix trie trimmedCmd 0 with | some incState => return some incState | none => return none diff --git a/REPL/Util/Trie.lean b/REPL/Util/Trie.lean new file mode 100644 index 00000000..b7c6b12f --- /dev/null +++ b/REPL/Util/Trie.lean @@ -0,0 +1,146 @@ +/- +Utilities for working with Lean's string Trie without deep recursion. +We provide iterative insert and matchPrefix to avoid stack overflows for +very long strings (e.g., multi-KB inputs). +-/ + +import Lean.Data.Trie + +namespace REPL.Util.Trie + +open Lean +open Lean.Data + +namespace Internal + +/-- Frames for rebuilding parent nodes after iteratively descending the trie. -/ +inductive Frame (α : Type) where + | node1 (v : Option α) (c : UInt8) : Frame α + | node (v : Option α) (cs : ByteArray) (ts : Array (Lean.Data.Trie α)) (idx : Nat) : Frame α + deriving Inhabited + +end Internal + +/-- Insert or replace the value at key `s` into trie `t` iteratively. -/ +def insert {α} (t : Lean.Data.Trie α) (s : String) (val : α) : Lean.Data.Trie α := + Id.run do + let bytes := s.toUTF8 + let n := bytes.size + + -- Build the suffix path from position `start` to the end of `s`. + let mkSuffixFrom (start : Nat) : Lean.Data.Trie α := + Id.run do + let mut r : Lean.Data.Trie α := Lean.Data.Trie.leaf (some val) + let mut j : Nat := n + while j > start do + let jp := j - 1 + let c := bytes.get! jp + r := Lean.Data.Trie.node1 none c r + j := jp + return r + + -- Descent state + let mut i : Nat := 0 + let mut cur : Lean.Data.Trie α := t + let mut stack : Array (Internal.Frame α) := #[] + + -- Iteratively descend until we either finish the key or need to branch/extend. + let mut done := false + let mut out := cur + while !done do + match cur with + | Lean.Data.Trie.leaf v => + if i < n then + let c := bytes.get! i + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node1 v c suffix + else + out := Lean.Data.Trie.leaf (some val) + done := true + | Lean.Data.Trie.node1 v c' t' => + if i < n then + let c := bytes.get! i + if c == c' then + stack := stack.push (Internal.Frame.node1 v c') + cur := t' + i := i + 1 + else + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node v (ByteArray.mk #[c, c']) (#[(suffix), t']) + done := true + else + out := Lean.Data.Trie.node1 (some val) c' t' + done := true + | Lean.Data.Trie.node v cs ts => + if i < n then + let c := bytes.get! i + match cs.findIdx? (· == c) with + | none => + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node v (cs.push c) (ts.push suffix) + done := true + | some idx => + stack := stack.push (Internal.Frame.node v cs ts idx) + cur := ts[idx]! + i := i + 1 + else + out := Lean.Data.Trie.node (some val) cs ts + done := true + + -- Rebuild parents from the stack + let mut res := out + for frame in stack.reverse do + match frame with + | Internal.Frame.node1 v c => + res := Lean.Data.Trie.node1 v c res + | Internal.Frame.node v cs ts idx => + res := Lean.Data.Trie.node v cs (ts.set! idx res) + return res + +/-- +Find the longest key in the trie that is contained in the given string `s` at position `i`, +and return the associated value, implemented iteratively to avoid stack overflows. + +Note the argument order is `(t s i)` to match usages in `Main.lean`. +-/ +def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos) : Option α := + Id.run do + let bytes := s.toUTF8 + let n := bytes.size + let mut idx : Nat := i.byteIdx + let mut cur : Lean.Data.Trie α := t + let mut best : Option α := none + let mut done := false + while !done do + match cur with + | Lean.Data.Trie.leaf v => + if v.isSome then + return v + else + return best + | Lean.Data.Trie.node1 v c' t' => + if v.isSome then best := v + if idx < n then + let c := bytes.get! idx + if c == c' then + idx := idx + 1 + cur := t' + else + done := true + else + done := true + | Lean.Data.Trie.node v cs ts => + if v.isSome then best := v + if idx < n then + let c := bytes.get! idx + match cs.findIdx? (· == c) with + | some j => + idx := idx + 1 + cur := ts[j]! + | none => + done := true + else + done := true + return best + +end REPL.Util.Trie From f6b9c1d33e701150954efda1997a2f13b00eb471 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 17/19] Make incrementality optional --- REPL/JSON.lean | 1 + REPL/Main.lean | 21 +++++++++++---------- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index fa44e2a8..70a7313f 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -19,6 +19,7 @@ structure CommandOptions where Anything else is ignored. -/ infotree : Option String + incrementality : Option Bool := none -- whether to use incremental mode optimization /-- Run Lean commands. If `env = none`, starts a new session (in which you can use `import`). diff --git a/REPL/Main.lean b/REPL/Main.lean index fb6a5e70..0ccec7d0 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -369,19 +369,20 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - -- Find the best incremental state to reuse based on prefix matching - let bestIncrementalState? ← findBestIncrementalState s.cmd s.env - - let (initialCmdState, incStates, messages, headerCache) ← try - IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache + let (initialCmdState, incStates, messages) ← try + if s.incrementality.getD false then + let bestIncrementalState? ← findBestIncrementalState s.cmd s.env + let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache + -- Store the command text and incremental states for future reuse + modify fun st => { st with headerCache := headerCache } + recordCommandIncrementals s.cmd incStates s.env + pure (initialCmdState, incStates, messages) + else + let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {} + pure (initialCmdState, incStates, messages) catch ex => return .inr ⟨ex.toString⟩ - modify fun st => { st with headerCache := headerCache } - - -- Store the command text and incremental states for future reuse - recordCommandIncrementals s.cmd incStates s.env - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From 759219e40701beb3b97fc23851c2eabf162e68c8 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 18/19] Update incrementality test --- test/Mathlib/test/incrementality.in | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in index 19bea50e..3e5c1738 100644 --- a/test/Mathlib/test/incrementality.in +++ b/test/Mathlib/test/incrementality.in @@ -1,5 +1,5 @@ -{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true, "incrementality": true} -{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true, "incrementality": true} -{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"} +{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added", "incrementality": true} From 9a415e8d00c273e05056f10bed6b5de06c6a45ca Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Wed, 22 Oct 2025 12:39:46 +0200 Subject: [PATCH 19/19] Fix compilation warning --- REPL/Util/Trie.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/REPL/Util/Trie.lean b/REPL/Util/Trie.lean index b7c6b12f..bf095237 100644 --- a/REPL/Util/Trie.lean +++ b/REPL/Util/Trie.lean @@ -103,7 +103,7 @@ and return the associated value, implemented iteratively to avoid stack overflow Note the argument order is `(t s i)` to match usages in `Main.lean`. -/ -def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos) : Option α := +def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos.Raw) : Option α := Id.run do let bytes := s.toUTF8 let n := bytes.size