From 1daf69eb1e7957a8d0a4cf1a94262e1bfd684042 Mon Sep 17 00:00:00 2001 From: Thomas Zhu Date: Mon, 23 Jun 2025 13:34:34 -0700 Subject: [PATCH 01/24] set local context in getProofStatus (triggered when continuing proof from allTactics and rootGoals) --- REPL/Main.lean | 3 ++- test/all_tactics-20250622.expected.out | 11 +++++++++++ test/all_tactics-20250622.in | 4 ++++ 3 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/all_tactics-20250622.expected.out create mode 100644 test/all_tactics-20250622.in diff --git a/REPL/Main.lean b/REPL/Main.lean index b00b6833..76d5578f 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -185,6 +185,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do let res := proofState.runMetaM do match proofState.rootGoals with | [goalId] => + goalId.withContext do match proofState.metaState.mctx.getExprAssignmentCore? goalId with | none => return "Error: Goal not assigned" | some pf => do @@ -196,7 +197,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 ← goalId.withContext $ abstractAllLambdaFVars pf + let pf ← abstractAllLambdaFVars pf let pft ← Meta.inferType pf >>= instantiateMVars if pf.hasExprMVar then diff --git a/test/all_tactics-20250622.expected.out b/test/all_tactics-20250622.expected.out new file mode 100644 index 00000000..3b16cd5b --- /dev/null +++ b/test/all_tactics-20250622.expected.out @@ -0,0 +1,11 @@ +{"tactics": + [{"usedConstants": [], + "tactic": "exact hp", + "proofState": 0, + "pos": {"line": 2, "column": 2}, + "goals": "P : Prop\nhp : P\n⊢ P", + "endPos": {"line": 2, "column": 10}}], + "env": 0} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + diff --git a/test/all_tactics-20250622.in b/test/all_tactics-20250622.in new file mode 100644 index 00000000..eeb5153e --- /dev/null +++ b/test/all_tactics-20250622.in @@ -0,0 +1,4 @@ +{"cmd": "example (P : Prop) (hp : P) : P := by\n exact hp\n", "allTactics": true} + +{"tactic": "exact hp", "proofState": 0} + From 5c7ace0bc1513fc8f8b8f75580b8759fd0b0cdf5 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 14:12:05 +0200 Subject: [PATCH 02/24] 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 76d5578f..d8a42d70 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 df967c3dc6dd02f948b2df5e43c367d336496fe1 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 14:24:15 +0200 Subject: [PATCH 03/24] 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 24ba3527bbc00a9376790a895006b9d71fb7f495 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 18:39:42 +0200 Subject: [PATCH 04/24] 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 24db8402..657f446d 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -46,7 +46,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 d8a42d70..2e5ae37e 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 7dd42c396203fde13040ab2f237ff804b0d24527 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 18:39:43 +0200 Subject: [PATCH 05/24] 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 2e5ae37e..a8e4791b 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 5cd5f78c52550a98f3ddc62e5e8097457f372a3b Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 18:39:44 +0200 Subject: [PATCH 06/24] 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 1a5843c7524e5146a16a87987608c0c1b15dce16 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 18:39:44 +0200 Subject: [PATCH 07/24] 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 1a3c38681a224edd76e16477ade31c75e496aff7 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Thu, 26 Jun 2025 18:41:34 +0200 Subject: [PATCH 08/24] 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 a8e4791b..d60bf861 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 17a1863a90c9e8dd42e178106bd1e40f3b684b93 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 27 Jun 2025 18:04:28 +0200 Subject: [PATCH 09/24] 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 03807f1a42d9ed233144d16e39ddb7d800cbf8bd Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 27 Jun 2025 18:04:50 +0200 Subject: [PATCH 10/24] 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 8a7e809c..46980117 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 d60bf861..f7afe622 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 056336f5899f3a587e20036432bcadcb2a56402e Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 27 Jun 2025 18:04:51 +0200 Subject: [PATCH 11/24] 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 46980117..24835a8e 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 f7afe622..1a910fd0 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 ce07834acad8889aa05eebaad5a34037417d753b Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Sat, 28 Jun 2025 09:23:48 +0200 Subject: [PATCH 12/24] 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 e702696b079d47a1775718b3ab473d3ec3bc824b Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Tue, 6 May 2025 23:34:10 +0100 Subject: [PATCH 13/24] Add initial working version that only works for tactic proofs --- REPL/JSON.lean | 9 +++++++++ REPL/Main.lean | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 657f446d..7a8c976c 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -188,4 +188,13 @@ structure UnpickleProofState where env : Option Nat deriving ToJson, FromJson +structure GetDeclType where + env: Option Nat + decl: String +deriving ToJson, FromJson + +structure DeclTypeResponse where + types: List String +deriving ToJson, FromJson + end REPL diff --git a/REPL/Main.lean b/REPL/Main.lean index 1a910fd0..48cf0b5c 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -355,6 +355,35 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState +def getDeclType (n: GetDeclType) : M IO (DeclTypeResponse ⊕ Error) := do + let (cmdSnapshot?, notFound) ← do match n.env with + | none => pure (none, false) + | some i => do match (← get).cmdStates[i]? with + | some env => pure (some env, false) + | none => pure (none, true) + if notFound then + return .inr ⟨"Unknown environment."⟩ + let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState + let (initialCmdState, cmdState, messages, trees) ← try + IO.processInput n.decl initialCmdState? + catch ex => + return .inr ⟨ex.toString⟩ + trees.forM fun t => do IO.println (← t.format) + IO.println (trees.map (fun t => (t.findRootGoals.length))) + + let optional_decls: List String ← trees.flatMap InfoTree.findRootGoals |>.mapM + fun ⟨t, ctx, goals⟩ => do + let mctx := ctx.mctx + let x := fun (m: MVarId) => do + let localContext : LocalContext := (← m.getDecl).lctx + match localContext.decls.get! 0 with + | none => pure "" + | some firstDecl => pure ((← Meta.ppExpr (← Lean.Meta.inferType firstDecl.toExpr)).pretty') + t.runMetaM ctx x + IO.println optional_decls + let decls := optional_decls.filter (fun s => !s.isEmpty) + return .inl (DeclTypeResponse.mk decls) + /-- Run a command, returning the id of the new environment, and any messages and sorries. -/ @@ -465,6 +494,7 @@ inductive Input | unpickleEnvironment : REPL.UnpickleEnvironment → Input | pickleProofSnapshot : REPL.PickleProofState → Input | unpickleProofSnapshot : REPL.UnpickleProofState → Input +| getDeclType : REPL.GetDeclType → Input /-- Parse a user input string to an input command. -/ def parse (query : String) : IO Input := do @@ -486,6 +516,8 @@ def parse (query : String) : IO Input := do | .ok (r : REPL.Command) => return .command r | .error _ => match fromJson? j with | .ok (r : REPL.File) => return .file r + | .error _ => match fromJson? j with + | .ok (r: REPL.GetDeclType) => return .getDeclType r | .error e => throw <| IO.userError <| toString <| toJson <| (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error) @@ -511,6 +543,7 @@ where loop : M IO Unit := do | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) + | .getDeclType r => return toJson (← getDeclType r) printFlush "\n" -- easier to parse the output if there are blank lines loop From 933f9cf2b8cec83cde6c3eee7c921582ed9c73ed Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Wed, 7 May 2025 01:06:17 +0100 Subject: [PATCH 14/24] Add working get decl type --- REPL/Lean/InfoTree.lean | 14 ++++++++++++++ REPL/Main.lean | 24 +++++++++--------------- test/gettype.expected.out | 6 ++++++ test/gettype.in | 5 +++++ 4 files changed, 34 insertions(+), 15 deletions(-) create mode 100644 test/gettype.expected.out create mode 100644 test/gettype.in diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 88da1b98..b7476d2f 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -190,6 +190,20 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals) | _ => none +/-- Returns all `TermInfo` nodes for a given `InfoTree`. -/ +partial def findTermNodes (t : InfoTree) (ctx? : Option ContextInfo := none) : + List (TermInfo × ContextInfo) := + match t with + | .context ctx t => t.findTermNodes (ctx.mergeIntoOuter? ctx?) + | .node info ts => + match info with + | .ofTermInfo i => + match ctx? with + | some ctx => [(i, ctx)] + | _ => [] + | _ => ts.toList.flatMap (fun t => t.findTermNodes ctx?) + | _ => [] + /-- Returns the root goals for a given `InfoTree`. -/ partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) : List (TacticInfo × ContextInfo × List MVarId) := diff --git a/REPL/Main.lean b/REPL/Main.lean index 48cf0b5c..50f09b21 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -364,25 +364,19 @@ def getDeclType (n: GetDeclType) : M IO (DeclTypeResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (initialCmdState, cmdState, messages, trees) ← try + let (_, _, _, trees) ← try IO.processInput n.decl initialCmdState? catch ex => return .inr ⟨ex.toString⟩ - trees.forM fun t => do IO.println (← t.format) - IO.println (trees.map (fun t => (t.findRootGoals.length))) - - let optional_decls: List String ← trees.flatMap InfoTree.findRootGoals |>.mapM - fun ⟨t, ctx, goals⟩ => do - let mctx := ctx.mctx - let x := fun (m: MVarId) => do - let localContext : LocalContext := (← m.getDecl).lctx - match localContext.decls.get! 0 with - | none => pure "" - | some firstDecl => pure ((← Meta.ppExpr (← Lean.Meta.inferType firstDecl.toExpr)).pretty') - t.runMetaM ctx x - IO.println optional_decls + let terms := trees.map InfoTree.findTermNodes + let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty') + let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst)) + let optional_decls: List String ← terms.mapM fun treeterms => do + match treeterms.getLast? with + | none => pure "" + | some a => inner a let decls := optional_decls.filter (fun s => !s.isEmpty) - return .inl (DeclTypeResponse.mk decls) + return .inl <| DeclTypeResponse.mk decls /-- Run a command, returning the id of the new environment, and any messages and sorries. diff --git a/test/gettype.expected.out b/test/gettype.expected.out new file mode 100644 index 00000000..4ff9d451 --- /dev/null +++ b/test/gettype.expected.out @@ -0,0 +1,6 @@ +{"types": ["∀ (p : Prop), p → p"]} + +{"types": ["∀ (p : Prop), p → p"]} + +{"types": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"]} + diff --git a/test/gettype.in b/test/gettype.in new file mode 100644 index 00000000..7a2917da --- /dev/null +++ b/test/gettype.in @@ -0,0 +1,5 @@ +{"decl": "theorem show_p (p : Prop) (h : p) : p := by exact h"} + +{"decl": "def show_q (p : Prop) (h : p) : p := h"} + +{"decl": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h"} From 7e1f722701ee8cbb9c22b168a9352d6de9ef6a55 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Wed, 7 May 2025 09:58:13 +0100 Subject: [PATCH 15/24] Add sorries and messages to DeclTypeResponse --- REPL/JSON.lean | 2 ++ REPL/Main.lean | 8 +++++--- test/gettype.expected.out | 14 +++++++++++--- test/transitive.in | 9 +++++++++ 4 files changed, 27 insertions(+), 6 deletions(-) create mode 100644 test/transitive.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 7a8c976c..c4b2fa23 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -195,6 +195,8 @@ deriving ToJson, FromJson structure DeclTypeResponse where types: List String + messages : List Message := [] + sorries : List Sorry := [] deriving ToJson, FromJson end REPL diff --git a/REPL/Main.lean b/REPL/Main.lean index 50f09b21..7ab0fc0d 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -364,10 +364,12 @@ def getDeclType (n: GetDeclType) : M IO (DeclTypeResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (_, _, _, trees) ← try + let (initialCmdState, _, messages, trees) ← try IO.processInput n.decl initialCmdState? catch ex => return .inr ⟨ex.toString⟩ + let messages ← messages.mapM fun m => Message.of m + let sorries ← sorries trees initialCmdState.env none let terms := trees.map InfoTree.findTermNodes let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty') let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst)) @@ -375,8 +377,8 @@ def getDeclType (n: GetDeclType) : M IO (DeclTypeResponse ⊕ Error) := do match treeterms.getLast? with | none => pure "" | some a => inner a - let decls := optional_decls.filter (fun s => !s.isEmpty) - return .inl <| DeclTypeResponse.mk decls + let types := optional_decls.filter (fun s => !s.isEmpty) + return .inl { types, messages, sorries } /-- Run a command, returning the id of the new environment, and any messages and sorries. diff --git a/test/gettype.expected.out b/test/gettype.expected.out index 4ff9d451..869f2aa9 100644 --- a/test/gettype.expected.out +++ b/test/gettype.expected.out @@ -1,6 +1,14 @@ -{"types": ["∀ (p : Prop), p → p"]} +{"types": ["∀ (p : Prop), p → p"], + "sorries": [], + "messages": + [{"severity": "info", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 51}, + "data": "Goals accomplished!"}]} -{"types": ["∀ (p : Prop), p → p"]} +{"types": ["∀ (p : Prop), p → p"], "sorries": [], "messages": []} -{"types": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"]} +{"types": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"], + "sorries": [], + "messages": []} diff --git a/test/transitive.in b/test/transitive.in new file mode 100644 index 00000000..4c030817 --- /dev/null +++ b/test/transitive.in @@ -0,0 +1,9 @@ +{"cmd": "theorem onelethree : 1 ≤ 3 := by sorry"} + +{"tactic": "apply Nat.le_trans", "proofState" : 0} + +{"tactic": "apply Nat.succ_le_succ", "proofState" : 1} + +{"cmd": "theorem onelethreetwo : 1 ≤ 3 := by sorry"} + +{"tactic": "apply (Nat.le_trans (m := 2))", "proofState" : 3} From 0e909093c8feb77e922bcc9627d3328704d0a345 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Wed, 7 May 2025 10:24:23 +0100 Subject: [PATCH 16/24] Add gettype test with variable --- test/gettype.expected.out | 9 +++++++++ test/gettype.in | 2 ++ 2 files changed, 11 insertions(+) diff --git a/test/gettype.expected.out b/test/gettype.expected.out index 869f2aa9..9c0e9e7c 100644 --- a/test/gettype.expected.out +++ b/test/gettype.expected.out @@ -12,3 +12,12 @@ "sorries": [], "messages": []} +{"types": ["Prop", "∀ (q : Prop), Type → q → q"], + "sorries": [], + "messages": + [{"severity": "warning", + "pos": {"line": 2, "column": 12}, + "endPos": {"line": 2, "column": 13}, + "data": + "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}]} + diff --git a/test/gettype.in b/test/gettype.in index 7a2917da..c4d9b573 100644 --- a/test/gettype.in +++ b/test/gettype.in @@ -3,3 +3,5 @@ {"decl": "def show_q (p : Prop) (h : p) : p := h"} {"decl": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h"} + +{"decl": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h"} From 4fe9ce1fa00f7168db55ea986774a4d23116c089 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Fri, 23 May 2025 14:15:30 +0100 Subject: [PATCH 17/24] Move declType to command options --- REPL/JSON.lean | 14 ++---- REPL/Main.lean | 45 +++++++------------ .../test/decltypenamespace.expected.out | 10 +++++ test/Mathlib/test/decltypenamespace.in | 3 ++ test/Mathlib/test/decltypeopen.expected.out | 10 +++++ test/Mathlib/test/decltypeopen.in | 3 ++ test/gettype.expected.out | 22 +++++---- test/gettype.in | 8 ++-- test/transitive.in | 9 ---- 9 files changed, 58 insertions(+), 66 deletions(-) create mode 100644 test/Mathlib/test/decltypenamespace.expected.out create mode 100644 test/Mathlib/test/decltypenamespace.in create mode 100644 test/Mathlib/test/decltypeopen.expected.out create mode 100644 test/Mathlib/test/decltypeopen.in delete mode 100644 test/transitive.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index c4b2fa23..33838955 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -13,6 +13,7 @@ namespace REPL structure CommandOptions where allTactics : Option Bool := none + declTypes: Option Bool := none rootGoals : Option Bool := none /-- Should be "full", "tactics", "original", or "substantive". @@ -125,6 +126,7 @@ structure CommandResponse where messages : List Message := [] sorries : List Sorry := [] tactics : List Tactic := [] + decls: List String := [] infotree : Option Json := none deriving FromJson @@ -138,6 +140,7 @@ instance : ToJson CommandResponse where Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "tactics" r.tactics, + Json.nonemptyList "decls" r.decls, match r.infotree with | some j => [("infotree", j)] | none => [] ] @@ -188,15 +191,4 @@ structure UnpickleProofState where env : Option Nat deriving ToJson, FromJson -structure GetDeclType where - env: Option Nat - decl: String -deriving ToJson, FromJson - -structure DeclTypeResponse where - types: List String - messages : List Message := [] - sorries : List Sorry := [] -deriving ToJson, FromJson - end REPL diff --git a/REPL/Main.lean b/REPL/Main.lean index 7ab0fc0d..499f1f99 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -187,6 +187,16 @@ def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv let restTactics ← tacticsCmd rest state.commandState.env return ts ++ restTactics +def declTypes (trees: List InfoTree) : M m (List String) := do + let terms := trees.map InfoTree.findTermNodes + let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty') + let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst)) + let optional_decls: List String ← terms.mapM fun treeterms => do + match treeterms.getLast? with + | none => pure "" + | some a => inner a + pure (optional_decls.filter (fun s => !s.isEmpty)) + def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do @@ -355,31 +365,6 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState -def getDeclType (n: GetDeclType) : M IO (DeclTypeResponse ⊕ Error) := do - let (cmdSnapshot?, notFound) ← do match n.env with - | none => pure (none, false) - | some i => do match (← get).cmdStates[i]? with - | some env => pure (some env, false) - | none => pure (none, true) - if notFound then - return .inr ⟨"Unknown environment."⟩ - let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (initialCmdState, _, messages, trees) ← try - IO.processInput n.decl initialCmdState? - catch ex => - return .inr ⟨ex.toString⟩ - let messages ← messages.mapM fun m => Message.of m - let sorries ← sorries trees initialCmdState.env none - let terms := trees.map InfoTree.findTermNodes - let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty') - let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst)) - let optional_decls: List String ← terms.mapM fun treeterms => do - match treeterms.getLast? with - | none => pure "" - | some a => inner a - let types := optional_decls.filter (fun s => !s.isEmpty) - return .inl { types, messages, sorries } - /-- Run a command, returning the id of the new environment, and any messages and sorries. -/ @@ -424,6 +409,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot let trees := cmdState.infoState.trees.toList + let decls ← match s.declTypes with + | some true => declTypes trees + | _ => pure [] -- 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 @@ -440,7 +428,8 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do { env, messages, sorries, - tactics + tactics, + decls, infotree } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do @@ -490,7 +479,6 @@ inductive Input | unpickleEnvironment : REPL.UnpickleEnvironment → Input | pickleProofSnapshot : REPL.PickleProofState → Input | unpickleProofSnapshot : REPL.UnpickleProofState → Input -| getDeclType : REPL.GetDeclType → Input /-- Parse a user input string to an input command. -/ def parse (query : String) : IO Input := do @@ -512,8 +500,6 @@ def parse (query : String) : IO Input := do | .ok (r : REPL.Command) => return .command r | .error _ => match fromJson? j with | .ok (r : REPL.File) => return .file r - | .error _ => match fromJson? j with - | .ok (r: REPL.GetDeclType) => return .getDeclType r | .error e => throw <| IO.userError <| toString <| toJson <| (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error) @@ -539,7 +525,6 @@ where loop : M IO Unit := do | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) - | .getDeclType r => return toJson (← getDeclType r) printFlush "\n" -- easier to parse the output if there are blank lines loop diff --git a/test/Mathlib/test/decltypenamespace.expected.out b/test/Mathlib/test/decltypenamespace.expected.out new file mode 100644 index 00000000..5353b9d6 --- /dev/null +++ b/test/Mathlib/test/decltypenamespace.expected.out @@ -0,0 +1,10 @@ +{"env": 0} + +{"messages": + [{"severity": "info", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 75}, + "data": "Goals accomplished!"}], + "env": 1, + "decls": ["∑ k ∈ Nat.properDivisors 198, k = 270"]} + diff --git a/test/Mathlib/test/decltypenamespace.in b/test/Mathlib/test/decltypenamespace.in new file mode 100644 index 00000000..da3aef58 --- /dev/null +++ b/test/Mathlib/test/decltypenamespace.in @@ -0,0 +1,3 @@ +{"cmd": "import Mathlib.NumberTheory.Divisors"} + +{"cmd": "theorem with_namespace : (∑ k ∈ Nat.properDivisors 198, k) = 270 := by rfl", "env": 0, "declTypes": true} diff --git a/test/Mathlib/test/decltypeopen.expected.out b/test/Mathlib/test/decltypeopen.expected.out new file mode 100644 index 00000000..df96a48b --- /dev/null +++ b/test/Mathlib/test/decltypeopen.expected.out @@ -0,0 +1,10 @@ +{"env": 0} + +{"messages": + [{"severity": "info", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 75}, + "data": "Goals accomplished!"}], + "env": 1, + "decls": ["∑ k ∈ properDivisors 198, k = 270"]} + diff --git a/test/Mathlib/test/decltypeopen.in b/test/Mathlib/test/decltypeopen.in new file mode 100644 index 00000000..9bf153fc --- /dev/null +++ b/test/Mathlib/test/decltypeopen.in @@ -0,0 +1,3 @@ +{"cmd": "import Mathlib.NumberTheory.Divisors\nopen Nat"} + +{"cmd": "theorem with_namespace : (∑ k ∈ Nat.properDivisors 198, k) = 270 := by rfl", "env": 0, "declTypes": true} diff --git a/test/gettype.expected.out b/test/gettype.expected.out index 9c0e9e7c..a7116be4 100644 --- a/test/gettype.expected.out +++ b/test/gettype.expected.out @@ -1,23 +1,21 @@ -{"types": ["∀ (p : Prop), p → p"], - "sorries": [], - "messages": +{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 51}, - "data": "Goals accomplished!"}]} + "data": "Goals accomplished!"}], + "env": 0, + "decls": ["∀ (p : Prop), p → p"]} -{"types": ["∀ (p : Prop), p → p"], "sorries": [], "messages": []} +{"env": 1, "decls": ["∀ (p : Prop), p → p"]} -{"types": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"], - "sorries": [], - "messages": []} +{"env": 2, "decls": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"]} -{"types": ["Prop", "∀ (q : Prop), Type → q → q"], - "sorries": [], - "messages": +{"messages": [{"severity": "warning", "pos": {"line": 2, "column": 12}, "endPos": {"line": 2, "column": 13}, "data": - "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}]} + "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}], + "env": 3, + "decls": ["Prop", "∀ (q : Prop), Type → q → q"]} diff --git a/test/gettype.in b/test/gettype.in index c4d9b573..1f296a89 100644 --- a/test/gettype.in +++ b/test/gettype.in @@ -1,7 +1,7 @@ -{"decl": "theorem show_p (p : Prop) (h : p) : p := by exact h"} +{"cmd": "theorem show_p (p : Prop) (h : p) : p := by exact h", "declTypes": true} -{"decl": "def show_q (p : Prop) (h : p) : p := h"} +{"cmd": "def show_q (p : Prop) (h : p) : p := h", "declTypes": true} -{"decl": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h"} +{"cmd": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h", "declTypes": true} -{"decl": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h"} +{"cmd": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h", "declTypes": true} diff --git a/test/transitive.in b/test/transitive.in deleted file mode 100644 index 4c030817..00000000 --- a/test/transitive.in +++ /dev/null @@ -1,9 +0,0 @@ -{"cmd": "theorem onelethree : 1 ≤ 3 := by sorry"} - -{"tactic": "apply Nat.le_trans", "proofState" : 0} - -{"tactic": "apply Nat.succ_le_succ", "proofState" : 1} - -{"cmd": "theorem onelethreetwo : 1 ≤ 3 := by sorry"} - -{"tactic": "apply (Nat.le_trans (m := 2))", "proofState" : 3} From e19af02799eae2adb3bc13c23415d6f388541305 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Fri, 23 May 2025 16:28:57 +0100 Subject: [PATCH 18/24] Add position info to declTypes --- REPL/JSON.lean | 16 ++++++++- REPL/Lean/InfoTree.lean | 8 +++++ REPL/Main.lean | 20 ++++++----- .../test/decltypenamespace.expected.out | 6 +++- test/Mathlib/test/decltypeopen.expected.out | 6 +++- test/gettype.expected.out | 34 ++++++++++++++++--- test/gettype.in | 2 +- 7 files changed, 75 insertions(+), 17 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 33838955..2b849e08 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -117,6 +117,20 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : proofState, usedConstants } +structure DeclType where + pos: Pos + endPos : Pos + type: String + pp: String +deriving ToJson, FromJson + +/-- Construct the JSON representation of a Declaration type. -/ +def DeclType.of (type pp : String) (pos endPos : Lean.Position) : DeclType := + { pos := ⟨pos.line, pos.column⟩, + endPos := ⟨endPos.line, endPos.column⟩, + type, + pp } + /-- A response to a Lean command. `env` can be used in later calls, to build on the stored environment. @@ -126,7 +140,7 @@ structure CommandResponse where messages : List Message := [] sorries : List Sorry := [] tactics : List Tactic := [] - decls: List String := [] + decls: List DeclType := [] infotree : Option Json := none deriving FromJson diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index b7476d2f..845d4c0c 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -272,6 +272,14 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List range.snd, i.getUsedConstantsAsSet.toArray ) +def declType (t : InfoTree) : Option (ContextInfo × Expr × Syntax × LocalContext × Position × Position) := + let terms: List (TermInfo × ContextInfo) := t.findTermNodes + match terms.getLast? with + | some ⟨i, ctx⟩ => + let range := stxRange ctx.fileMap i.stx + (ctx, i.expr, i.stx, i.lctx, range.fst, range.snd) + | _ => none + def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) := t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ => let range := stxRange ctx.fileMap i.stx diff --git a/REPL/Main.lean b/REPL/Main.lean index 499f1f99..2e486593 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -187,15 +187,17 @@ def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv let restTactics ← tacticsCmd rest state.commandState.env return ts ++ restTactics -def declTypes (trees: List InfoTree) : M m (List String) := do - let terms := trees.map InfoTree.findTermNodes - let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty') - let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst)) - let optional_decls: List String ← terms.mapM fun treeterms => do - match treeterms.getLast? with - | none => pure "" - | some a => inner a - pure (optional_decls.filter (fun s => !s.isEmpty)) +def declTypes (trees: List InfoTree) : M m (List DeclType) := do + let exprType: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.inferType expr)).pretty' + let treeDecl := (fun t => do + let dt := InfoTree.declType t + match dt with + | some ⟨ctx, expr, stx, lctx, pos, endPos⟩ => + let type := (← ctx.runMetaM lctx (exprType expr)) + let pp := Format.pretty stx.prettyPrint + pure [DeclType.of type pp pos endPos] + | _ => pure []) + trees.flatMapM treeDecl def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM diff --git a/test/Mathlib/test/decltypenamespace.expected.out b/test/Mathlib/test/decltypenamespace.expected.out index 5353b9d6..5b9a352e 100644 --- a/test/Mathlib/test/decltypenamespace.expected.out +++ b/test/Mathlib/test/decltypenamespace.expected.out @@ -6,5 +6,9 @@ "endPos": {"line": 1, "column": 75}, "data": "Goals accomplished!"}], "env": 1, - "decls": ["∑ k ∈ Nat.properDivisors 198, k = 270"]} + "decls": + [{"type": "∑ k ∈ Nat.properDivisors 198, k = 270", + "pp": "with_namespace", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 22}}]} diff --git a/test/Mathlib/test/decltypeopen.expected.out b/test/Mathlib/test/decltypeopen.expected.out index df96a48b..3c555459 100644 --- a/test/Mathlib/test/decltypeopen.expected.out +++ b/test/Mathlib/test/decltypeopen.expected.out @@ -6,5 +6,9 @@ "endPos": {"line": 1, "column": 75}, "data": "Goals accomplished!"}], "env": 1, - "decls": ["∑ k ∈ properDivisors 198, k = 270"]} + "decls": + [{"type": "∑ k ∈ properDivisors 198, k = 270", + "pp": "with_namespace", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 22}}]} diff --git a/test/gettype.expected.out b/test/gettype.expected.out index a7116be4..b1b4b129 100644 --- a/test/gettype.expected.out +++ b/test/gettype.expected.out @@ -4,11 +4,29 @@ "endPos": {"line": 1, "column": 51}, "data": "Goals accomplished!"}], "env": 0, - "decls": ["∀ (p : Prop), p → p"]} + "decls": + [{"type": "∀ (p : Prop), p → p", + "pp": "show_p", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 14}}]} -{"env": 1, "decls": ["∀ (p : Prop), p → p"]} +{"env": 1, + "decls": + [{"type": "∀ (p : Prop), p → p", + "pp": "show_q", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 10}}]} -{"env": 2, "decls": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"]} +{"env": 2, + "decls": + [{"type": "∀ (p : Prop), p → p", + "pp": "show_p", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 10}}, + {"type": "∀ (q : Prop), q → q", + "pp": "show_q", + "pos": {"line": 3, "column": 4}, + "endPos": {"line": 3, "column": 10}}]} {"messages": [{"severity": "warning", @@ -17,5 +35,13 @@ "data": "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 3, - "decls": ["Prop", "∀ (q : Prop), Type → q → q"]} + "decls": + [{"type": "Prop", + "pp": "q", + "pos": {"line": 1, "column": 10}, + "endPos": {"line": 1, "column": 11}}, + {"type": "∀ (q : Prop), Type → q → q", + "pp": "show_q", + "pos": {"line": 2, "column": 4}, + "endPos": {"line": 2, "column": 10}}]} diff --git a/test/gettype.in b/test/gettype.in index 1f296a89..8d274dcb 100644 --- a/test/gettype.in +++ b/test/gettype.in @@ -2,6 +2,6 @@ {"cmd": "def show_q (p : Prop) (h : p) : p := h", "declTypes": true} -{"cmd": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h", "declTypes": true} +{"cmd": "def show_p (p : Prop) (h : p) : p := h\n\ndef show_q (q : Prop) (h : q) : q := h", "declTypes": true} {"cmd": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h", "declTypes": true} From a50fce61066f16be2fabb233467f4a7b940b084b Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Sat, 24 May 2025 11:41:45 +0100 Subject: [PATCH 19/24] Add namespace flag --- REPL/JSON.lean | 24 +++++++++-- REPL/Lean/InfoTree.lean | 45 ++++++++++++++++---- REPL/Main.lean | 12 ++++++ test/namespaces.expected.out | 41 +++++++++++++++++++ test/namespaces.in | 3 ++ test/sections.expected.out | 79 ++++++++++++++++++++++++++++++++++++ test/sections.in | 5 +++ 7 files changed, 197 insertions(+), 12 deletions(-) create mode 100644 test/namespaces.expected.out create mode 100644 test/namespaces.in create mode 100644 test/sections.expected.out create mode 100644 test/sections.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 2b849e08..de2c8c84 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -14,6 +14,7 @@ namespace REPL structure CommandOptions where allTactics : Option Bool := none declTypes: Option Bool := none + namespaces: Option Bool := none rootGoals : Option Bool := none /-- Should be "full", "tactics", "original", or "substantive". @@ -118,10 +119,10 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : usedConstants } structure DeclType where - pos: Pos + pos : Pos endPos : Pos - type: String - pp: String + type : String + pp : String deriving ToJson, FromJson /-- Construct the JSON representation of a Declaration type. -/ @@ -131,6 +132,21 @@ def DeclType.of (type pp : String) (pos endPos : Lean.Position) : DeclType := type, pp } +structure Namespace where + pos : Pos + endPos : Pos + currentNamespace : String + openDecls: List String + pp : String +deriving ToJson, FromJson + +def Namespace.of (currentNamespace pp : String) (openDecls : List String) (pos endPos : Lean.Position) : Namespace := + { pos := ⟨pos.line, pos.column⟩, + endPos := ⟨endPos.line, endPos.column⟩, + currentNamespace, + openDecls, + pp } + /-- A response to a Lean command. `env` can be used in later calls, to build on the stored environment. @@ -141,6 +157,7 @@ structure CommandResponse where sorries : List Sorry := [] tactics : List Tactic := [] decls: List DeclType := [] + namespaces: List Namespace := [] infotree : Option Json := none deriving FromJson @@ -155,6 +172,7 @@ instance : ToJson CommandResponse where Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "tactics" r.tactics, Json.nonemptyList "decls" r.decls, + Json.nonemptyList "namespaces" r.namespaces, match r.infotree with | some j => [("infotree", j)] | none => [] ] diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 845d4c0c..6a8c25db 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -193,16 +193,31 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa /-- Returns all `TermInfo` nodes for a given `InfoTree`. -/ partial def findTermNodes (t : InfoTree) (ctx? : Option ContextInfo := none) : List (TermInfo × ContextInfo) := - match t with - | .context ctx t => t.findTermNodes (ctx.mergeIntoOuter? ctx?) - | .node info ts => + let infoCtx := t.findAllInfo ctx? fun (info: Info) => match info with - | .ofTermInfo i => - match ctx? with - | some ctx => [(i, ctx)] - | _ => [] - | _ => ts.toList.flatMap (fun t => t.findTermNodes ctx?) - | _ => [] + | .ofTermInfo _ => true + | _ => false + infoCtx.flatMap fun ⟨info, ctx?⟩ => + match info with + | .ofTermInfo i => match ctx? with + | some ctx => [(i, ctx)] + | _ => [] + | _ => [] + + +/-- Returns all `CommandInfo` nodes for a given `InfoTree`. -/ +partial def findCommandNodes (t : InfoTree) (ctx? : Option ContextInfo := none) : + List (CommandInfo × ContextInfo) := + let infoCtx := t.findAllInfo ctx? fun (info: Info) => + match info with + | .ofCommandInfo _ => true + | _ => false + infoCtx.flatMap fun ⟨info, ctx?⟩ => + match info with + | .ofCommandInfo i => match ctx? with + | some ctx => [(i, ctx)] + | _ => [] + | _ => [] /-- Returns the root goals for a given `InfoTree`. -/ partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) : @@ -280,6 +295,18 @@ def declType (t : InfoTree) : Option (ContextInfo × Expr × Syntax × LocalCont (ctx, i.expr, i.stx, i.lctx, range.fst, range.snd) | _ => none +def namespaces (t : InfoTree) : List (CommandInfo × ContextInfo × Position × Position) := + let nodes := t.findCommandNodes |>.filter fun ⟨i, _⟩ => + match i.elaborator with + | ``Lean.Elab.Command.elabOpen => true + | ``Lean.Elab.Command.elabSection => true + | ``Lean.Elab.Command.elabEnd => true + | ``Lean.Elab.Command.elabNamespace => true + | _ => false + nodes.map fun ⟨i, ctx⟩ => + let range := stxRange ctx.fileMap i.stx + (i, ctx, range.fst, range.snd) + def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) := t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ => let range := stxRange ctx.fileMap i.stx diff --git a/REPL/Main.lean b/REPL/Main.lean index 2e486593..07d3132f 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -199,6 +199,14 @@ def declTypes (trees: List InfoTree) : M m (List DeclType) := do | _ => pure []) trees.flatMapM treeDecl +def namespaces (trees: List InfoTree) : M m (List Namespace) := + trees.flatMap InfoTree.namespaces |>.mapM + fun ⟨i, ctx, pos, endPos⟩ => + let openDecls: List String := ctx.openDecls.map toString + let pp := (Format.pretty i.stx.prettyPrint) + let currNamespace := toString ctx.currNamespace + pure (Namespace.of currNamespace pp openDecls pos endPos) + def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do @@ -402,6 +410,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let tactics ← match s.allTactics with | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] + let namespaces ← match s.namespaces with + | some true => namespaces trees + | _ => pure [] let cmdSnapshot := { cmdState cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD @@ -432,6 +443,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do sorries, tactics, decls, + namespaces, infotree } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do diff --git a/test/namespaces.expected.out b/test/namespaces.expected.out new file mode 100644 index 00000000..00ac54f9 --- /dev/null +++ b/test/namespaces.expected.out @@ -0,0 +1,41 @@ +{"namespaces": + [{"pp": "namespace Lean", + "pos": {"line": 1, "column": 0}, + "openDecls": [], + "endPos": {"line": 1, "column": 14}, + "currentNamespace": "Lean"}, + {"pp": "open Nat", + "pos": {"line": 2, "column": 0}, + "openDecls": ["Nat"], + "endPos": {"line": 2, "column": 8}, + "currentNamespace": "Lean"}, + {"pp": "open Elab", + "pos": {"line": 3, "column": 0}, + "openDecls": ["Lean.Elab", "Nat"], + "endPos": {"line": 3, "column": 9}, + "currentNamespace": "Lean"}], + "env": 0} + +{"namespaces": + [{"pp": "open Lean", + "pos": {"line": 1, "column": 0}, + "openDecls": ["Lean", "Lean.Elab", "Nat"], + "endPos": {"line": 1, "column": 9}, + "currentNamespace": "Lean"}, + {"pp": "section test", + "pos": {"line": 2, "column": 0}, + "openDecls": ["Lean", "Lean.Elab", "Nat"], + "endPos": {"line": 2, "column": 12}, + "currentNamespace": "Lean"}, + {"pp": "open Nat", + "pos": {"line": 3, "column": 0}, + "openDecls": ["Nat", "Lean", "Lean.Elab", "Nat"], + "endPos": {"line": 3, "column": 8}, + "currentNamespace": "Lean"}, + {"pp": "end test", + "pos": {"line": 4, "column": 0}, + "openDecls": ["Lean", "Lean.Elab", "Nat"], + "endPos": {"line": 4, "column": 8}, + "currentNamespace": "Lean"}], + "env": 1} + diff --git a/test/namespaces.in b/test/namespaces.in new file mode 100644 index 00000000..c2ef97ea --- /dev/null +++ b/test/namespaces.in @@ -0,0 +1,3 @@ +{"cmd": "namespace Lean\nopen Nat\nopen Elab", "namespaces": true} + +{"cmd": "open Lean\nsection test\nopen Nat\nend test", "namespaces": true, "env": 0} diff --git a/test/sections.expected.out b/test/sections.expected.out new file mode 100644 index 00000000..5ff601e3 --- /dev/null +++ b/test/sections.expected.out @@ -0,0 +1,79 @@ +{"namespaces": + [{"pp": "section", + "pos": {"line": 1, "column": 0}, + "openDecls": [], + "endPos": {"line": 1, "column": 7}, + "currentNamespace": "[anonymous]"}, + {"pp": "open Nat", + "pos": {"line": 2, "column": 0}, + "openDecls": ["Nat"], + "endPos": {"line": 2, "column": 8}, + "currentNamespace": "[anonymous]"}, + {"pp": "end", + "pos": {"line": 3, "column": 0}, + "openDecls": [], + "endPos": {"line": 3, "column": 3}, + "currentNamespace": "[anonymous]"}], + "env": 0} + +{"namespaces": + [{"pp": "open Lean", + "pos": {"line": 1, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 1, "column": 9}, + "currentNamespace": "[anonymous]"}, + {"pp": "section test", + "pos": {"line": 2, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 2, "column": 12}, + "currentNamespace": "[anonymous]"}, + {"pp": "open Nat", + "pos": {"line": 3, "column": 0}, + "openDecls": ["Nat", "Lean"], + "endPos": {"line": 3, "column": 8}, + "currentNamespace": "[anonymous]"}, + {"pp": "end test", + "pos": {"line": 4, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 4, "column": 8}, + "currentNamespace": "[anonymous]"}], + "env": 1} + +{"namespaces": + [{"pp": "open Lean", + "pos": {"line": 1, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 1, "column": 9}, + "currentNamespace": "[anonymous]"}, + {"pp": "section", + "pos": {"line": 2, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 2, "column": 7}, + "currentNamespace": "[anonymous]"}, + {"pp": "open Nat", + "pos": {"line": 3, "column": 0}, + "openDecls": ["Nat", "Lean"], + "endPos": {"line": 3, "column": 8}, + "currentNamespace": "[anonymous]"}, + {"pp": "section test", + "pos": {"line": 4, "column": 0}, + "openDecls": ["Nat", "Lean"], + "endPos": {"line": 4, "column": 12}, + "currentNamespace": "[anonymous]"}, + {"pp": "open Elab", + "pos": {"line": 5, "column": 0}, + "openDecls": ["Lean.Elab", "Nat", "Lean"], + "endPos": {"line": 5, "column": 9}, + "currentNamespace": "[anonymous]"}, + {"pp": "end test", + "pos": {"line": 6, "column": 0}, + "openDecls": ["Nat", "Lean"], + "endPos": {"line": 6, "column": 8}, + "currentNamespace": "[anonymous]"}, + {"pp": "end", + "pos": {"line": 7, "column": 0}, + "openDecls": ["Lean"], + "endPos": {"line": 7, "column": 3}, + "currentNamespace": "[anonymous]"}], + "env": 2} + diff --git a/test/sections.in b/test/sections.in new file mode 100644 index 00000000..ab64af73 --- /dev/null +++ b/test/sections.in @@ -0,0 +1,5 @@ +{"cmd": "section\nopen Nat\nend", "namespaces": true} + +{"cmd": "open Lean\nsection test\nopen Nat\nend test", "namespaces": true} + +{"cmd": "open Lean\nsection\nopen Nat\nsection test\nopen Elab\nend test\nend", "namespaces": true} From 4511a5679cad5fafa2d2926f6cc2ab2330728e99 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Tue, 1 Jul 2025 07:54:02 +0000 Subject: [PATCH 20/24] Move namespaces correctly --- REPL/Main.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 07d3132f..f92fa306 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -410,9 +410,6 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let tactics ← match s.allTactics with | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] - let namespaces ← match s.namespaces with - | some true => namespaces trees - | _ => pure [] let cmdSnapshot := { cmdState cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD @@ -425,6 +422,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let decls ← match s.declTypes with | some true => declTypes trees | _ => pure [] + let namespaces ← match s.namespaces with + | some true => namespaces trees + | _ => pure [] -- 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 524cac86507962cbec9d6d0b41bf658f93a23013 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Tue, 1 Jul 2025 10:27:44 +0000 Subject: [PATCH 21/24] Initial draft for conclusion splitting --- REPL/JSON.lean | 11 +++++++ REPL/Lean/InfoTree.lean | 64 ++++++++++++++++++++++++++++++++++--- REPL/Main.lean | 18 +++++++++++ test/full_tree.expected.out | 6 ++++ test/full_tree.in | 5 +++ test/gettype.expected.out | 9 ++---- 6 files changed, 102 insertions(+), 11 deletions(-) create mode 100644 test/full_tree.expected.out create mode 100644 test/full_tree.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index de2c8c84..ed4c1bd2 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -16,6 +16,7 @@ structure CommandOptions where declTypes: Option Bool := none namespaces: Option Bool := none rootGoals : Option Bool := none + conclusions : Option Bool := none /-- Should be "full", "tactics", "original", or "substantive". Anything else is ignored. @@ -146,6 +147,14 @@ def Namespace.of (currentNamespace pp : String) (openDecls : List String) (pos e currentNamespace, openDecls, pp } +structure Conclusion where + pos : Pos + endPos : Pos + pp: String +deriving FromJson, ToJson + +def Conclusion.of (pp : String) (pos endPos : Lean.Position) : Conclusion := + {pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, pp := pp} /-- A response to a Lean command. @@ -158,6 +167,7 @@ structure CommandResponse where tactics : List Tactic := [] decls: List DeclType := [] namespaces: List Namespace := [] + conclusions : List Conclusion := [] infotree : Option Json := none deriving FromJson @@ -173,6 +183,7 @@ instance : ToJson CommandResponse where Json.nonemptyList "tactics" r.tactics, Json.nonemptyList "decls" r.decls, Json.nonemptyList "namespaces" r.namespaces, + Json.nonemptyList "conclusions" r.conclusions, match r.infotree with | some j => [("infotree", j)] | none => [] ] diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 6a8c25db..0cb04585 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -130,14 +130,17 @@ Keep `.node` nodes and `.hole` nodes satisfying predicates. Returns a `List InfoTree`, although in most situations this will be a singleton. -/ -partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : +partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) (stopfun: Info → Bool := fun _ => false) : InfoTree → List InfoTree - | .context ctx tree => tree.filter p m |>.map (.context ctx) + | .context ctx tree => tree.filter p m stopfun |>.map (.context ctx) | .node info children => if p info then - [.node info (children.toList.map (filter p m)).flatten.toPArray'] + if stopfun info then + [.node info children] + else + [.node info (children.toList.map (filter p m stopfun)).flatten.toPArray'] else - (children.toList.map (filter p m)).flatten + if stopfun info then children.toList else (children.toList.map (filter p m stopfun)).flatten | .hole mvar => if m mvar then [.hole mvar] else [] /-- Discard all nodes besides `.context` nodes and `TacticInfo` nodes. -/ @@ -307,6 +310,59 @@ def namespaces (t : InfoTree) : List (CommandInfo × ContextInfo × Position × let range := stxRange ctx.fileMap i.stx (i, ctx, range.fst, range.snd) +-- Get the TermInfo with the largest position in the file +partial def maxTermNode (terms: List (TermInfo × Option ContextInfo)) : Option (TermInfo × ContextInfo) := + match terms.head? with + | some ⟨ti, ctx?⟩ => + let largestTail := maxTermNode terms.tail + match largestTail with + | some ⟨tailinfo, tailctx⟩ => + match ctx? with + | some ctx => + let range := stxRange ctx.fileMap ti.stx + let tailRange := stxRange tailctx.fileMap tailinfo.stx + if tailRange.snd.line > range.snd.line then some ⟨tailinfo, tailctx⟩ + else + if tailRange.snd.column > range.snd.column then some ⟨tailinfo, tailctx⟩ + else some ⟨ti, ctx⟩ + | none => some ⟨tailinfo, tailctx⟩ + | none => match ctx? with + | some ctx => some ⟨ti, ctx⟩ + | none => none + | none => none + +def child_len (t : InfoTree) : Nat := + match t with + | .context ctx k => child_len k + | .node i ts => ts.toList.length + | _ => 0 + +def conclusion (t : InfoTree) : IO (List (TermInfo × ContextInfo)) := do + let only_declarations := fun i => match i with + | .ofCommandInfo m => m.elaborator == ``Lean.Elab.Command.elabDeclaration + | _ => false + let only_term := fun i => match i with + | .ofTermInfo _ => true + | _ => false + + let trees := t.filter (fun i => only_declarations i) (stopfun := only_declarations) + trees.forM fun k => do IO.println (← k.format) + --let kmasdf := trees.map child_len + --IO.println s!"Length: {kmasdf}" + + let terms_info : List (List (Info × Option ContextInfo)) := trees.map <| fun t => t.findAllInfo none only_term (stop := fun i => Bool.not <| only_declarations i) + terms_info.forM fun t => t.forM (fun k => do IO.println k.fst.stx.prettyPrint) + let terms: List (List (TermInfo × Option ContextInfo)) := terms_info.map <| fun t => t.flatMap (fun ⟨i, ctx?⟩ => + match i with + | .ofTermInfo ti => [⟨ti, ctx?⟩] + | _ => []) + + let optional_conclusions := terms.map <| fun ts => maxTermNode ts + pure (optional_conclusions.flatMap <| fun c => + match c with + | some s => [s] + | _ => []) + def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) := t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ => let range := stxRange ctx.fileMap i.stx diff --git a/REPL/Main.lean b/REPL/Main.lean index f92fa306..2563e97b 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -207,6 +207,17 @@ def namespaces (trees: List InfoTree) : M m (List Namespace) := let currNamespace := toString ctx.currNamespace pure (Namespace.of currNamespace pp openDecls pos endPos) +def conclusions (trees: List InfoTree) : M m (List Conclusion) := do + let treeDecl := (fun t => do + let conc ← InfoTree.conclusion t + IO.println conc.length + conc.flatMapM <| fun ⟨info, ctx⟩ => do + let pp := Format.pretty info.stx.prettyPrint + let range := stxRange ctx.fileMap info.stx + pure [Conclusion.of pp range.fst range.snd]) + trees.flatMapM treeDecl + + def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do @@ -419,12 +430,18 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot let trees := cmdState.infoState.trees.toList + let decls ← match s.declTypes with | some true => declTypes trees | _ => pure [] let namespaces ← match s.namespaces with | some true => namespaces trees | _ => pure [] + let conclusions ← match s.conclusions with + | true => conclusions trees + | _ => pure [] + conclusions.forM fun t => do IO.println t.pp + -- 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 @@ -444,6 +461,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do tactics, decls, namespaces, + conclusions, infotree } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do diff --git a/test/full_tree.expected.out b/test/full_tree.expected.out new file mode 100644 index 00000000..c35df9bd --- /dev/null +++ b/test/full_tree.expected.out @@ -0,0 +1,6 @@ +{"env": 0, + "conclusions": + [{"pp": "1 + 1 = 2", + "pos": {"line": 1, "column": 12}, + "endPos": {"line": 1, "column": 21}}]} + diff --git a/test/full_tree.in b/test/full_tree.in new file mode 100644 index 00000000..c63cdbd4 --- /dev/null +++ b/test/full_tree.in @@ -0,0 +1,5 @@ +{"cmd": "theorem f : 1 + 1 = 2 := rfl", "conclusions": true, "infotree": "full"} + +{"cmd": "example (P : Prop) (hp : P) : P := by\n exact hp\n", "conclusions": true, "infotree": "full"} + +{"cmd": "variable (a : Prop)\ntheorem f (b : Prop) (hb : b) : Or a b := by\nright\nexact hb", "infotree": "full", "conclusions": true} diff --git a/test/gettype.expected.out b/test/gettype.expected.out index b1b4b129..359a33c1 100644 --- a/test/gettype.expected.out +++ b/test/gettype.expected.out @@ -1,9 +1,4 @@ -{"messages": - [{"severity": "info", - "pos": {"line": 1, "column": 0}, - "endPos": {"line": 1, "column": 51}, - "data": "Goals accomplished!"}], - "env": 0, +{"env": 0, "decls": [{"type": "∀ (p : Prop), p → p", "pp": "show_p", @@ -40,7 +35,7 @@ "pp": "q", "pos": {"line": 1, "column": 10}, "endPos": {"line": 1, "column": 11}}, - {"type": "∀ (q : Prop), Type → q → q", + {"type": "∀ (q : Prop) (p : Type), q → q", "pp": "show_q", "pos": {"line": 2, "column": 4}, "endPos": {"line": 2, "column": 10}}]} From 1833d0d0ee2218e6b4ca18dca989f48755e20756 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Tue, 1 Jul 2025 11:49:02 +0000 Subject: [PATCH 22/24] Cleanup --- REPL/Lean/InfoTree.lean | 34 +++++++++++++++------------------- REPL/Main.lean | 1 - test/full_tree.in | 10 +++++++--- 3 files changed, 22 insertions(+), 23 deletions(-) diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 0cb04585..0ced074b 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -130,17 +130,17 @@ Keep `.node` nodes and `.hole` nodes satisfying predicates. Returns a `List InfoTree`, although in most situations this will be a singleton. -/ -partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) (stopfun: Info → Bool := fun _ => false) : +partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) (stop: Info → Bool := fun _ => false) : InfoTree → List InfoTree - | .context ctx tree => tree.filter p m stopfun |>.map (.context ctx) + | .context ctx tree => tree.filter p m stop |>.map (.context ctx) | .node info children => if p info then - if stopfun info then + if stop info then [.node info children] else - [.node info (children.toList.map (filter p m stopfun)).flatten.toPArray'] + [.node info (children.toList.map (filter p m stop)).flatten.toPArray'] else - if stopfun info then children.toList else (children.toList.map (filter p m stopfun)).flatten + if stop info then children.toList else (children.toList.map (filter p m stop)).flatten | .hole mvar => if m mvar then [.hole mvar] else [] /-- Discard all nodes besides `.context` nodes and `TacticInfo` nodes. -/ @@ -331,30 +331,26 @@ partial def maxTermNode (terms: List (TermInfo × Option ContextInfo)) : Option | none => none | none => none -def child_len (t : InfoTree) : Nat := - match t with - | .context ctx k => child_len k - | .node i ts => ts.toList.length - | _ => 0 - def conclusion (t : InfoTree) : IO (List (TermInfo × ContextInfo)) := do let only_declarations := fun i => match i with - | .ofCommandInfo m => m.elaborator == ``Lean.Elab.Command.elabDeclaration + | .ofCommandInfo m => if m.elaborator == ``Lean.Elab.Command.elabDeclaration then + match m.stx.getArgs.toList.getLast? with + | some stx => stx.getKind == ``Lean.Parser.Command.theorem + | none => false + else false | _ => false let only_term := fun i => match i with | .ofTermInfo _ => true | _ => false - let trees := t.filter (fun i => only_declarations i) (stopfun := only_declarations) - trees.forM fun k => do IO.println (← k.format) - --let kmasdf := trees.map child_len - --IO.println s!"Length: {kmasdf}" - + let trees := t.filter (fun i => only_declarations i) (stop := only_declarations) let terms_info : List (List (Info × Option ContextInfo)) := trees.map <| fun t => t.findAllInfo none only_term (stop := fun i => Bool.not <| only_declarations i) - terms_info.forM fun t => t.forM (fun k => do IO.println k.fst.stx.prettyPrint) + let terms: List (List (TermInfo × Option ContextInfo)) := terms_info.map <| fun t => t.flatMap (fun ⟨i, ctx?⟩ => match i with - | .ofTermInfo ti => [⟨ti, ctx?⟩] + | .ofTermInfo ti => match ti.stx.getHeadInfo with + | .original .. => [⟨ti, ctx?⟩] + | _ => [] | _ => []) let optional_conclusions := terms.map <| fun ts => maxTermNode ts diff --git a/REPL/Main.lean b/REPL/Main.lean index 2563e97b..43b8c85a 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -210,7 +210,6 @@ def namespaces (trees: List InfoTree) : M m (List Namespace) := def conclusions (trees: List InfoTree) : M m (List Conclusion) := do let treeDecl := (fun t => do let conc ← InfoTree.conclusion t - IO.println conc.length conc.flatMapM <| fun ⟨info, ctx⟩ => do let pp := Format.pretty info.stx.prettyPrint let range := stxRange ctx.fileMap info.stx diff --git a/test/full_tree.in b/test/full_tree.in index c63cdbd4..072bf394 100644 --- a/test/full_tree.in +++ b/test/full_tree.in @@ -1,5 +1,9 @@ -{"cmd": "theorem f : 1 + 1 = 2 := rfl", "conclusions": true, "infotree": "full"} +{"cmd": "theorem f : 1 + 1 = 2 := rfl", "conclusions": true} -{"cmd": "example (P : Prop) (hp : P) : P := by\n exact hp\n", "conclusions": true, "infotree": "full"} +{"cmd": "example (P : Prop) (hp : P) : P := by\n exact hp\n", "conclusions": true} -{"cmd": "variable (a : Prop)\ntheorem f (b : Prop) (hb : b) : Or a b := by\nright\nexact hb", "infotree": "full", "conclusions": true} +{"cmd": "variable (a : Prop)\ntheorem f (b : Prop) (hb : b) : Or a b := by\nright\nexact hb", "conclusions": true} + +{"cmd": "def f := 37", "conclusions": true} + +{"cmd": "theorem a_and_b (a b : Prop) (ha : a) (hb : b) : ∃ (c : Nat), c = 2 := by simp", "conclusions": true} \ No newline at end of file From 70aa7e382229e6d48f57aebd2eeec4b6508c64a1 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Tue, 1 Jul 2025 11:55:57 +0000 Subject: [PATCH 23/24] Add working test --- REPL/Main.lean | 2 +- test/conclusion.expected.out | 33 ++++++++++++++++++++++++++++ test/{full_tree.in => conclusion.in} | 2 +- test/full_tree.expected.out | 6 ----- 4 files changed, 35 insertions(+), 8 deletions(-) create mode 100644 test/conclusion.expected.out rename test/{full_tree.in => conclusion.in} (88%) delete mode 100644 test/full_tree.expected.out diff --git a/REPL/Main.lean b/REPL/Main.lean index 43b8c85a..16bd72fa 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -439,7 +439,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let conclusions ← match s.conclusions with | true => conclusions trees | _ => pure [] - conclusions.forM fun t => do IO.println t.pp + -- conclusions.forM fun t => do IO.println t.pp -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) diff --git a/test/conclusion.expected.out b/test/conclusion.expected.out new file mode 100644 index 00000000..d058ad33 --- /dev/null +++ b/test/conclusion.expected.out @@ -0,0 +1,33 @@ +{"env": 0, + "conclusions": + [{"pp": "1 + 1 = 2", + "pos": {"line": 1, "column": 12}, + "endPos": {"line": 1, "column": 21}}]} + +{"env": 1} + +{"env": 2, + "conclusions": + [{"pp": "Or a b", + "pos": {"line": 2, "column": 32}, + "endPos": {"line": 2, "column": 38}}]} + +{"env": 3} + +{"messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 30}, + "endPos": {"line": 1, "column": 32}, + "data": + "unused variable `ha`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}, + {"severity": "warning", + "pos": {"line": 1, "column": 39}, + "endPos": {"line": 1, "column": 41}, + "data": + "unused variable `hb`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}], + "env": 4, + "conclusions": + [{"pp": "∃ (c : Nat), c = 2", + "pos": {"line": 1, "column": 49}, + "endPos": {"line": 1, "column": 67}}]} + diff --git a/test/full_tree.in b/test/conclusion.in similarity index 88% rename from test/full_tree.in rename to test/conclusion.in index 072bf394..af77dd63 100644 --- a/test/full_tree.in +++ b/test/conclusion.in @@ -6,4 +6,4 @@ {"cmd": "def f := 37", "conclusions": true} -{"cmd": "theorem a_and_b (a b : Prop) (ha : a) (hb : b) : ∃ (c : Nat), c = 2 := by simp", "conclusions": true} \ No newline at end of file +{"cmd": "theorem a_and_b (a b : Prop) (ha : a) (hb : b) : ∃ (c : Nat), c = 2 := by simp", "conclusions": true} diff --git a/test/full_tree.expected.out b/test/full_tree.expected.out deleted file mode 100644 index c35df9bd..00000000 --- a/test/full_tree.expected.out +++ /dev/null @@ -1,6 +0,0 @@ -{"env": 0, - "conclusions": - [{"pp": "1 + 1 = 2", - "pos": {"line": 1, "column": 12}, - "endPos": {"line": 1, "column": 21}}]} - From e18d3c9d2b5c752f8b9729669d877cea52d697e4 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Fri, 4 Jul 2025 13:21:51 +0000 Subject: [PATCH 24/24] Add conclusion to decltype --- REPL/JSON.lean | 6 ++++-- REPL/Main.lean | 4 +++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ed4c1bd2..303384cd 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -124,14 +124,16 @@ structure DeclType where endPos : Pos type : String pp : String + conclusion : String deriving ToJson, FromJson /-- Construct the JSON representation of a Declaration type. -/ -def DeclType.of (type pp : String) (pos endPos : Lean.Position) : DeclType := +def DeclType.of (type pp conclusion : String) (pos endPos : Lean.Position) : DeclType := { pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, type, - pp } + pp + conclusion } structure Namespace where pos : Pos diff --git a/REPL/Main.lean b/REPL/Main.lean index 16bd72fa..4fbca112 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -189,13 +189,15 @@ def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv def declTypes (trees: List InfoTree) : M m (List DeclType) := do let exprType: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.inferType expr)).pretty' + let conclusion: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.forallMetaTelescope (← Meta.inferType expr)).snd.snd).pretty' let treeDecl := (fun t => do let dt := InfoTree.declType t match dt with | some ⟨ctx, expr, stx, lctx, pos, endPos⟩ => let type := (← ctx.runMetaM lctx (exprType expr)) let pp := Format.pretty stx.prettyPrint - pure [DeclType.of type pp pos endPos] + let conclusionStr ← ctx.runMetaM lctx <| conclusion expr + pure [DeclType.of type pp conclusionStr pos endPos] | _ => pure []) trees.flatMapM treeDecl