From 73b5b390b0d116740bba09bc2c5f145ec0b39f9a Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:41 +0100 Subject: [PATCH 01/27] Improve `LocalContext` and `LocalInstance` extraction for sorries --- REPL/Main.lean | 8 ++------ REPL/Snapshots.lean | 49 +++++++++++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 25 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index b05583f7..88455968 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op fun ⟨ctx, g, pos, endPos⟩ => do let (goal, proofState) ← match g with | .tactic g => do - let lctx ← ctx.runMetaM {} do - match ctx.mctx.findDecl? g with - | some decl => return decl.lctx - | none => throwError "unknown metavariable '{g}'" - let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals? + let s ← ProofSnapshot.create ctx none env? [g] rootGoals? pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term lctx (some t) => do let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] @@ -197,7 +193,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do unless (← Meta.isDefEq pft expectedType) do return s!"Error: proof has type {pft} but root goal has type {expectedType}" - let pf ← abstractAllLambdaFVars pf + let pf ← abstractAllLambdaFVars pf >>= instantiateMVars let pft ← Meta.inferType pf >>= instantiateMVars if pf.hasExprMVar then diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index f6936245..e5ddd9a6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·) + /-- Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals. - For convenience, we also allow a list of `Expr`s, and these are appended to the goals as fresh metavariables with the given types. -/ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do - ctx.runMetaM (lctx?.getD {}) do - let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } - pure <| - { coreState := s - coreContext := ← readThe Core.Context - metaState := ← getThe Meta.State - metaContext := ← readThe Meta.Context - termState := {} - termContext := {} - tacticState := { goals } - tacticContext := { elaborator := .anonymous } - rootGoals := match rootGoals? with - | none => goals - | some gs => gs } + -- Get the local context from the goals if not provided. + let lctx ← match lctx? with + | none => match goals with + | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx + | [] => match rootGoals? with + | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx + | _ => pure {} + | some lctx => pure lctx + + ctx.runMetaM lctx do + -- update local instances, which is necessary when `types` is non-empty + Meta.withLocalInstances (lctx.decls.toList.filterMap id) do + let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) + let s ← getThe Core.State + let s := match env? with + | none => s + | some env => { s with env } + pure <| + { coreState := s + coreContext := ← readThe Core.Context + metaState := ← getThe Meta.State + metaContext := ← readThe Meta.Context + termState := {} + termContext := {} + tacticState := { goals } + tacticContext := { elaborator := .anonymous } + rootGoals := match rootGoals? with + | none => goals + | some gs => gs } open Lean.Core in /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/ From b57b7dacbbc0ab974e692a359b79954f882af190 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 17 Nov 2025 09:38:42 +0100 Subject: [PATCH 02/27] Add test --- test/local_instance_proof.expected.out | 62 ++++++++++++++++++++++++++ test/local_instance_proof.in | 21 +++++++++ 2 files changed, 83 insertions(+) create mode 100644 test/local_instance_proof.expected.out create mode 100644 test/local_instance_proof.in diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out new file mode 100644 index 00000000..5a93d082 --- /dev/null +++ b/test/local_instance_proof.expected.out @@ -0,0 +1,62 @@ +{"env": 0} + +{"env": 1} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 42}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 47}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"sorries": + [{"proofState": 2, + "pos": {"line": 1, "column": 45}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 50}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 3} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"env": 4} + +{"sorries": + [{"proofState": 4, + "pos": {"line": 1, "column": 17}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 22}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 5} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + +{"sorries": + [{"proofState": 6, + "pos": {"line": 1, "column": 20}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 25}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 6} + +{"proofStatus": "Completed", "proofState": 7, "goals": []} + diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in new file mode 100644 index 00000000..eeefd5ef --- /dev/null +++ b/test/local_instance_proof.in @@ -0,0 +1,21 @@ +{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 2} + +{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0} + +{"cmd": "def test2 : α := sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 4} + +{"cmd": "def test2 : α := by sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 6} From b28f3b78a886c98a4ea55ac7e217cd29beebe792 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:12 +0200 Subject: [PATCH 03/27] First attempt at doing incremental processing of commands --- REPL/Frontend.lean | 60 +++++++++++++++--------- REPL/JSON.lean | 2 +- REPL/Main.lean | 71 +++++++++++++++++++---------- test/pattern_match.expected.out | 6 +++ test/pattern_match.in | 6 +++ test/self_proof_check2.expected.out | 0 test/self_proof_check2.in | 6 +++ 7 files changed, 106 insertions(+), 45 deletions(-) create mode 100644 test/pattern_match.expected.out create mode 100644 test/pattern_match.in create mode 100644 test/self_proof_check2.expected.out create mode 100644 test/self_proof_check2.in diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 81575ed3..54ceeb25 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -9,6 +9,31 @@ open Lean Elab namespace Lean.Elab.IO +partial def filterRootTactics (tree : InfoTree) : Bool := + match tree with + | InfoTree.hole _ => true + | InfoTree.context _ t => filterRootTactics t + | InfoTree.node i _ => match i with + | .ofTacticInfo _ => false + | _ => true + +/-- Traverses a command snapshot tree, yielding each intermediate state. -/ +partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot) +(prevCmdState : Command.State) : + IO (List ((List InfoTree) × Command.State)) := do + let tree := Language.toSnapshotTree snap + let snapshots := tree.getAll + let infotrees := snapshots.map (·.infoTree?) + let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics + let results := [(infotrees, snap.resultSnap.task.get.cmdState)] + -- let results := [(infotrees, prevCmdState)] + match snap.nextCmdSnap? with + | none => return results + | some nextSnapTask => + let nextSnap := nextSnapTask.task.get + let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState + return results ++ nextResults + /-- Wrapper for `IO.processCommands` that enables info states, and returns * the new command state @@ -17,41 +42,34 @@ Wrapper for `IO.processCommands` that enables info states, and returns -/ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) - (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do + (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do let commandState := { commandState with infoState.enabled := true } - let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState - pure (s, s.messages.toList, s.infoState.trees.toList) + let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none + let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState + let s := incs.commandState + pure (s, s.messages.toList, infoTrees) /-- Process some text input, with or without an existing command state. -If there is no existing environment, we parse the input for headers (e.g. import statements), -and create a new environment. -Otherwise, we add to the existing environment. Returns: -1. The header-only command state (only useful when cmdState? is none) -2. The resulting command state after processing the entire input -3. List of messages -4. List of info trees +1. The resulting command state after processing the entire input +2. List of messages +3. List of info trees along with Command.State from the incremental processing -/ def processInput (input : String) (cmdState? : Option Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do + IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName - match cmdState? with + let (parserState, commandState) ← match cmdState? with | none => do - -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx - let headerOnlyState := Command.mkState env messages opts - let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState - return (headerOnlyState, cmdState, messages, trees) - - | some cmdStateBefore => do - let parserState : Parser.ModuleParserState := {} - let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore - return (cmdStateBefore, cmdStateAfter, messages, trees) + pure (parserState, (Command.mkState env messages opts)) + | some cmdState => do + pure ({ : Parser.ModuleParserState }, cmdState) + processCommandsWithInfoTrees inputCtx parserState commandState diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..fa44e2a8 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -47,7 +47,7 @@ deriving ToJson, FromJson structure Pos where line : Nat column : Nat -deriving ToJson, FromJson +deriving ToJson, FromJson, BEq, Hashable /-- Severity of a message. -/ inductive Severity diff --git a/REPL/Main.lean b/REPL/Main.lean index 88455968..3377ae3b 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -111,29 +111,53 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goal pos endPos proofStateId +-- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +-- : M m (List Sorry) := do +-- -- Create a hash set to track positions we've already seen +-- let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {} +-- let mut result : List Sorry := [] + +-- for (trees, cmdState) in treeList do +-- let newSorries ← sorries trees cmdState.env rootGoals? + +-- -- Add only sorries at positions we haven't seen yet +-- for sorr in newSorries do +-- let pos := (sorr.pos, sorr.endPos) +-- unless seenPositions.contains pos do +-- seenPositions := seenPositions.insert pos +-- result := sorr :: result + +-- return result + +def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +: M m (List Sorry) := + treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals? + def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try Lean.PrettyPrinter.ppTactic ⟨stx⟩ catch _ => pure "" -def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) := - trees.flatMap InfoTree.tactics |>.mapM - fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let tactic := Format.pretty (← ppTactic ctx stx) - let proofStateId ← proofState.mapM recordProofSnapshot - return Tactic.of goals tactic pos endPos proofStateId ns - -def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do - trees.flatMap InfoTree.rootGoals |>.mapM - fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none env? goals goals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId - +def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) := + treeList.flatMapM fun (trees, cmdState) => do + trees.flatMap InfoTree.tactics |>.mapM + fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do + let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let tactic := Format.pretty (← ppTactic ctx stx) + let proofStateId ← proofState.mapM recordProofSnapshot + return Tactic.of goals tactic pos endPos proofStateId ns + +def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State)) +: M m (List Sorry) := do + treeList.flatMapM fun (trees, cmdState) => do + trees.flatMap InfoTree.rootGoals |>.mapM + fun ⟨ctx, goals, pos⟩ => do + let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let proofStateId ← proofState.mapM recordProofSnapshot + return Sorry.of goals pos pos proofStateId private def collectFVarsAux : Expr → NameSet | .fvar fvarId => NameSet.empty.insert fvarId.name @@ -298,19 +322,17 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (initialCmdState, cmdState, messages, trees) ← try + let (cmdState, messages, trees) ← try IO.processInput s.cmd initialCmdState? catch ex => return .inr ⟨ex.toString⟩ let messages ← messages.mapM fun m => Message.of m - -- For debugging purposes, sometimes we print out the trees here: - -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees initialCmdState.env none + let sorries ← sorries2 trees none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics trees initialCmdState.env + | some true => tactics trees | _ => pure [] let cmdSnapshot := { cmdState @@ -320,6 +342,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do snap? := none, cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot + let trees := (trees.map (·.1)).flatten + -- For debugging purposes, sometimes we print out the trees here: + -- trees.forM fun t => do IO.println (← t.format) let jsonTrees := match s.infotree with | some "full" => trees | some "tactics" => trees.flatMap InfoTree.retainTacticInfo diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out new file mode 100644 index 00000000..2c1d028e --- /dev/null +++ b/test/pattern_match.expected.out @@ -0,0 +1,6 @@ +{"cmd": "#eval 1 + 1"} + +{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} + +{"tactic": "simp", "proofState": 0} + diff --git a/test/pattern_match.in b/test/pattern_match.in new file mode 100644 index 00000000..2c1d028e --- /dev/null +++ b/test/pattern_match.in @@ -0,0 +1,6 @@ +{"cmd": "#eval 1 + 1"} + +{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} + +{"tactic": "simp", "proofState": 0} + diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out new file mode 100644 index 00000000..e69de29b diff --git a/test/self_proof_check2.in b/test/self_proof_check2.in new file mode 100644 index 00000000..78c0b6a9 --- /dev/null +++ b/test/self_proof_check2.in @@ -0,0 +1,6 @@ +{"cmd": "theorem x : False := sorry\nexample : False := by exact?"} + +{"cmd": "theorem x : False := sorry\nexample : False := sorry"} + +{"proofState": 2, "tactic": "exact?"} + From f402fd8878e834c95150e1bcd6c896ade126625c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 04/27] Implement incrmental collection of sorries --- REPL/Frontend.lean | 83 +++++++++++++++++++++++++--------------------- REPL/Main.lean | 63 +++++++++++++++++------------------ 2 files changed, 76 insertions(+), 70 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 54ceeb25..8a7e809c 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -5,34 +5,41 @@ Authors: Scott Morrison -/ import Lean.Elab.Frontend -open Lean Elab +open Lean Elab Language namespace Lean.Elab.IO -partial def filterRootTactics (tree : InfoTree) : Bool := - match tree with - | InfoTree.hole _ => true - | InfoTree.context _ t => filterRootTactics t - | InfoTree.node i _ => match i with - | .ofTacticInfo _ => false - | _ => true - -/-- Traverses a command snapshot tree, yielding each intermediate state. -/ -partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot) -(prevCmdState : Command.State) : - IO (List ((List InfoTree) × Command.State)) := do - let tree := Language.toSnapshotTree snap - let snapshots := tree.getAll - let infotrees := snapshots.map (·.infoTree?) - let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics - let results := [(infotrees, snap.resultSnap.task.get.cmdState)] - -- let results := [(infotrees, prevCmdState)] - match snap.nextCmdSnap? with - | none => return results - | some nextSnapTask => - let nextSnap := nextSnapTask.task.get - let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState - return results ++ nextResults +partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext) + (parserState : Parser.ModuleParserState) (commandState : Command.State) + (old? : Option IncrementalState) : + BaseIO (List (IncrementalState × Option InfoTree)) := do + let task ← Language.Lean.processCommands inputCtx parserState commandState + (old?.map fun old => (old.inputCtx, old.initialSnap)) + return go task.get task #[] +where + go initialSnap t commands := + let snap := t.get + let commands := commands.push snap + -- Opting into reuse also enables incremental reporting, so make sure to collect messages from + -- all snapshots + let messages := toSnapshotTree initialSnap + |>.getAll.map (·.diagnostics.msgLog) + |>.foldl (· ++ ·) {} + -- In contrast to messages, we should collect info trees only from the top-level command + -- snapshots as they subsume any info trees reported incrementally by their children. + let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let result : (IncrementalState × Option InfoTree) := + ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees } + , parserState := snap.parserState + , cmdPos := snap.parserState.pos + , commands := commands.map (·.stx) + , inputCtx := inputCtx + , initialSnap := initialSnap + }, snap.infoTreeSnap.get.infoTree?) + if let some next := snap.nextCmdSnap? then + result :: go initialSnap next.task commands + else + [result] /-- Wrapper for `IO.processCommands` that enables info states, and returns @@ -42,12 +49,11 @@ Wrapper for `IO.processCommands` that enables info states, and returns -/ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) - (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do + (commandState : Command.State) (incrementalState? : Option IncrementalState := none) + : IO (List (IncrementalState × Option InfoTree) × List Message) := do let commandState := { commandState with infoState.enabled := true } - let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none - let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState - let s := incs.commandState - pure (s, s.messages.toList, infoTrees) + let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState? + pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {}) /-- Process some text input, with or without an existing command state. @@ -59,17 +65,20 @@ Returns: -/ def processInput (input : String) (cmdState? : Option Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do + IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName - - let (parserState, commandState) ← match cmdState? with + match cmdState? with | none => do + -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx - pure (parserState, (Command.mkState env messages opts)) - | some cmdState => do - pure ({ : Parser.ModuleParserState }, cmdState) - processCommandsWithInfoTrees inputCtx parserState commandState + let headerOnlyState := Command.mkState env messages opts + let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState + return (headerOnlyState, incStates) + | some cmdStateBefore => do + let parserState : Parser.ModuleParserState := {} + let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore + return (cmdStateBefore, incStates) diff --git a/REPL/Main.lean b/REPL/Main.lean index 3377ae3b..449eabd4 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -111,27 +111,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goal pos endPos proofStateId --- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) --- : M m (List Sorry) := do --- -- Create a hash set to track positions we've already seen --- let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {} --- let mut result : List Sorry := [] - --- for (trees, cmdState) in treeList do --- let newSorries ← sorries trees cmdState.env rootGoals? - --- -- Add only sorries at positions we haven't seen yet --- for sorr in newSorries do --- let pos := (sorr.pos, sorr.endPos) --- unless seenPositions.contains pos do --- seenPositions := seenPositions.insert pos --- result := sorr :: result - --- return result - -def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId)) +def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) +(rootGoals? : Option (List MVarId)) : M m (List Sorry) := - treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals? + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let s ← sorries infoTree?.toList prevEnv rootGoals? + let restSorries ← sorriesCmd rest state.commandState.env rootGoals? + return s ++ restSorries def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try @@ -139,22 +127,22 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := catch _ => pure "" -def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) := - treeList.flatMapM fun (trees, cmdState) => do - trees.flatMap InfoTree.tactics |>.mapM +def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) := + treeList.flatMapM fun (state, infoTree?) => do + infoTree?.toList.flatMap InfoTree.tactics |>.mapM fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals) + let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals) let goals := s!"{(← ctx.ppGoals goals)}".trim let tactic := Format.pretty (← ppTactic ctx stx) let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns -def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State)) +def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree)) : M m (List Sorry) := do - treeList.flatMapM fun (trees, cmdState) => do - trees.flatMap InfoTree.rootGoals |>.mapM + treeList.flatMapM fun (state, infoTree?) => do + infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals) + let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals) let goals := s!"{(← ctx.ppGoals goals)}".trim let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goals pos pos proofStateId @@ -322,17 +310,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (cmdState, messages, trees) ← try + let (initialCmdState, incStates, messages) ← try IO.processInput s.cmd initialCmdState? catch ex => return .inr ⟨ex.toString⟩ + + let mut prevPos := 0 + for (incState, _) in incStates do + let endPos := incState.cmdPos + let processedText := incState.inputCtx.input.extract prevPos endPos + IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}" + prevPos := endPos + + let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m - let sorries ← sorries2 trees none + let sorries ← sorriesCmd incStates initialCmdState.env none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics trees + | some true => tactics incStates | _ => pure [] let cmdSnapshot := { cmdState @@ -342,7 +339,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do snap? := none, cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot - let trees := (trees.map (·.1)).flatten + let trees := cmdState.infoState.trees.toList -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) let jsonTrees := match s.infotree with From e252f5758d14396e1b72f417304643cc60a545bc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 05/27] Fix test output --- test/self_proof_check2.expected.out | 49 +++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out index e69de29b..99d5339f 100644 --- a/test/self_proof_check2.expected.out +++ b/test/self_proof_check2.expected.out @@ -0,0 +1,49 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "info", + "pos": {"line": 2, "column": 22}, + "endPos": {"line": 2, "column": 28}, + "data": "Try this: exact x"}, + {"severity": "info", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 28}, + "data": "Goals accomplished!"}], + "env": 0} + +{"sorries": + [{"proofState": 1, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}, + {"proofState": 2, + "pos": {"line": 2, "column": 19}, + "goal": "⊢ False", + "endPos": {"line": 2, "column": 24}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "warning", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": "Completed", + "proofState": 3, + "messages": + [{"severity": "info", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "Try this: exact x"}], + "goals": []} + From 849f8679d94afaeac7922faad487b6e4e23ee906 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:13 +0200 Subject: [PATCH 06/27] Update tests --- ...out => in_command_dependency.expected.out} | 6 +--- ...oof_check2.in => in_command_dependency.in} | 0 test/pattern_match.expected.out | 28 +++++++++++++++++-- test/pattern_match.in | 9 ++++-- 4 files changed, 33 insertions(+), 10 deletions(-) rename test/{self_proof_check2.expected.out => in_command_dependency.expected.out} (87%) rename test/{self_proof_check2.in => in_command_dependency.in} (100%) diff --git a/test/self_proof_check2.expected.out b/test/in_command_dependency.expected.out similarity index 87% rename from test/self_proof_check2.expected.out rename to test/in_command_dependency.expected.out index 99d5339f..e3ba5583 100644 --- a/test/self_proof_check2.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,11 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this: exact x"}, - {"severity": "info", - "pos": {"line": 2, "column": 0}, - "endPos": {"line": 2, "column": 28}, - "data": "Goals accomplished!"}], + "data": "Try this: exact x"}], "env": 0} {"sorries": diff --git a/test/self_proof_check2.in b/test/in_command_dependency.in similarity index 100% rename from test/self_proof_check2.in rename to test/in_command_dependency.in diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out index 2c1d028e..2e16d41f 100644 --- a/test/pattern_match.expected.out +++ b/test/pattern_match.expected.out @@ -1,6 +1,28 @@ -{"cmd": "#eval 1 + 1"} +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 77}, + "goal": + "⊢ (fun x =>\n match x with\n | (x, fst, snd) => x = x) =\n fun x => True", + "endPos": {"line": 1, "column": 82}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} -{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": + ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]} -{"tactic": "simp", "proofState": 0} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"proofStatus": "Completed", "proofState": 4, "goals": []} + +{"env": 1} diff --git a/test/pattern_match.in b/test/pattern_match.in index 2c1d028e..a863f0b9 100644 --- a/test/pattern_match.in +++ b/test/pattern_match.in @@ -1,6 +1,11 @@ -{"cmd": "#eval 1 + 1"} +{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"} -{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0} +{"tactic": "funext ⟨x, y, z⟩", "proofState": 0} + +{"tactic": "show (x = x) = True", "proofState": 1} + +{"tactic": "rw [eq_self_iff_true]", "proofState": 2} {"tactic": "simp", "proofState": 0} +{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"} From 5b795ed0be04631ee9eb75ae1b49168a55882a86 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:14 +0200 Subject: [PATCH 07/27] Improving fine-grained environment --- REPL/Main.lean | 63 +++++++++++++++++++++++++-------------------- REPL/Snapshots.lean | 33 +++++++++++++++++++----- 2 files changed, 62 insertions(+), 34 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 449eabd4..078c44b5 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -127,25 +127,39 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := catch _ => pure "" -def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) := - treeList.flatMapM fun (state, infoTree?) => do - infoTree?.toList.flatMap InfoTree.tactics |>.mapM - fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let tactic := Format.pretty (← ppTactic ctx stx) - let proofStateId ← proofState.mapM recordProofSnapshot - return Tactic.of goals tactic pos endPos proofStateId ns - -def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree)) -: M m (List Sorry) := do - treeList.flatMapM fun (state, infoTree?) => do - infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM - fun ⟨ctx, goals, pos⟩ => do - let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals) - let goals := s!"{(← ctx.ppGoals goals)}".trim - let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId +def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) := + trees.flatMap InfoTree.tactics |>.mapM + fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do + let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let tactic := Format.pretty (← ppTactic ctx stx) + let proofStateId ← proofState.mapM recordProofSnapshot + return Tactic.of goals tactic pos endPos proofStateId ns + +def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let ts ← tactics infoTree?.toList prevEnv + let restTactics ← tacticsCmd rest state.commandState.env + return ts ++ restTactics + +def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do + trees.flatMap InfoTree.rootGoals |>.mapM + fun ⟨ctx, goals, pos⟩ => do + let proofState := some (← ProofSnapshot.create ctx none env? goals goals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let proofStateId ← proofState.mapM recordProofSnapshot + return Sorry.of goals pos pos proofStateId + +def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : + M m (List Sorry) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv + let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env + return sorries ++ restSorries private def collectFVarsAux : Expr → NameSet | .fvar fvarId => NameSet.empty.insert fvarId.name @@ -315,21 +329,14 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do catch ex => return .inr ⟨ex.toString⟩ - let mut prevPos := 0 - for (incState, _) in incStates do - let endPos := incState.cmdPos - let processedText := incState.inputCtx.input.extract prevPos endPos - IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}" - prevPos := endPos - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics incStates + | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] let cmdSnapshot := { cmdState diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index e5ddd9a6..4fd6cfdb 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -191,7 +191,7 @@ Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, an For convenience, we also allow a list of `Expr`s, and these are appended to the goals as fresh metavariables with the given types. -/ -def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) +def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do -- Get the local context from the goals if not provided. @@ -207,12 +207,33 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi -- update local instances, which is necessary when `types` is non-empty Meta.withLocalInstances (lctx.decls.toList.filterMap id) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } + + -- Create a filtered environment that excludes the new (non-auxiliary) declarations + -- Necessary to avoid self-references in proofs in tactic mode, while still allowing + -- auxiliary declarations to be used in the proof. + let coreState ← match prevEnv? with + | none => getThe Core.State + | some prevEnv => do + let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName) + let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n + + let currentConsts := ctx.env.constants.map₂.toList + let prevConsts := prevEnv.constants.map₂.toList + let diff := currentConsts.filter (fun (name, _) => + !prevConsts.any (fun (name', _) => name == name')) + let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name + + -- Print for debugging purposes + IO.println s!"Constants to filter: {declsToFilter}" + IO.println s!"Replayed constants: {filteredConstants.map (·.1)}" + + let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants) + -- let filteredEnv := prevEnv + let s ← getThe Core.State + pure { s with env := filteredEnv } + pure <| - { coreState := s + { coreState := coreState coreContext := ← readThe Core.Context metaState := ← getThe Meta.State metaContext := ← readThe Meta.Context From 0fcfed993cd9222fdfa7d6dc62ac240f110a7740 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:14 +0200 Subject: [PATCH 08/27] Revert constant replay --- REPL/Snapshots.lean | 31 +++++-------------------------- test/pattern_match.expected.out | 28 ---------------------------- test/pattern_match.in | 11 ----------- 3 files changed, 5 insertions(+), 65 deletions(-) delete mode 100644 test/pattern_match.expected.out delete mode 100644 test/pattern_match.in diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 4fd6cfdb..d87981e6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -207,33 +207,12 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option -- update local instances, which is necessary when `types` is non-empty Meta.withLocalInstances (lctx.decls.toList.filterMap id) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - - -- Create a filtered environment that excludes the new (non-auxiliary) declarations - -- Necessary to avoid self-references in proofs in tactic mode, while still allowing - -- auxiliary declarations to be used in the proof. - let coreState ← match prevEnv? with - | none => getThe Core.State - | some prevEnv => do - let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName) - let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n - - let currentConsts := ctx.env.constants.map₂.toList - let prevConsts := prevEnv.constants.map₂.toList - let diff := currentConsts.filter (fun (name, _) => - !prevConsts.any (fun (name', _) => name == name')) - let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name - - -- Print for debugging purposes - IO.println s!"Constants to filter: {declsToFilter}" - IO.println s!"Replayed constants: {filteredConstants.map (·.1)}" - - let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants) - -- let filteredEnv := prevEnv - let s ← getThe Core.State - pure { s with env := filteredEnv } - + let s ← getThe Core.State + let s := match prevEnv? with + | none => s + | some env => { s with env } pure <| - { coreState := coreState + { coreState := s coreContext := ← readThe Core.Context metaState := ← getThe Meta.State metaContext := ← readThe Meta.Context diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out deleted file mode 100644 index 2e16d41f..00000000 --- a/test/pattern_match.expected.out +++ /dev/null @@ -1,28 +0,0 @@ -{"sorries": - [{"proofState": 0, - "pos": {"line": 1, "column": 77}, - "goal": - "⊢ (fun x =>\n match x with\n | (x, fst, snd) => x = x) =\n fun x => True", - "endPos": {"line": 1, "column": 82}}], - "messages": - [{"severity": "warning", - "pos": {"line": 1, "column": 4}, - "endPos": {"line": 1, "column": 7}, - "data": "declaration uses 'sorry'"}], - "env": 0} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 1, - "goals": - ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 2, - "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]} - -{"proofStatus": "Completed", "proofState": 3, "goals": []} - -{"proofStatus": "Completed", "proofState": 4, "goals": []} - -{"env": 1} - diff --git a/test/pattern_match.in b/test/pattern_match.in deleted file mode 100644 index a863f0b9..00000000 --- a/test/pattern_match.in +++ /dev/null @@ -1,11 +0,0 @@ -{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"} - -{"tactic": "funext ⟨x, y, z⟩", "proofState": 0} - -{"tactic": "show (x = x) = True", "proofState": 1} - -{"tactic": "rw [eq_self_iff_true]", "proofState": 2} - -{"tactic": "simp", "proofState": 0} - -{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"} From f33a50eb214cb9325641cbb83591f1b4ea2e97cc Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:28:15 +0200 Subject: [PATCH 09/27] Fix v4.22.0-rc2 --- REPL/Frontend.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 8a7e809c..bc2dff1e 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -27,15 +27,15 @@ where |>.foldl (· ++ ·) {} -- In contrast to messages, we should collect info trees only from the top-level command -- snapshots as they subsume any info trees reported incrementally by their children. - let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' let result : (IncrementalState × Option InfoTree) := - ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees } + ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees } , parserState := snap.parserState , cmdPos := snap.parserState.pos , commands := commands.map (·.stx) , inputCtx := inputCtx , initialSnap := initialSnap - }, snap.infoTreeSnap.get.infoTree?) + }, snap.elabSnap.infoTreeSnap.get.infoTree?) if let some next := snap.nextCmdSnap? then result :: go initialSnap next.task commands else From 98d737c2c0cb1c4e1a035593d72778d7ca5e5115 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:24 +0200 Subject: [PATCH 10/27] Fix test v4.24.0-rc1 --- test/in_command_dependency.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out index e3ba5583..66371d34 100644 --- a/test/in_command_dependency.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,7 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this: exact x"}], + "data": "Try this:\n exact x"}], "env": 0} {"sorries": @@ -40,6 +40,6 @@ [{"severity": "info", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "Try this: exact x"}], + "data": "Try this:\n exact x"}], "goals": []} From 4d97344f3e2571a541e2f95dd01147b5f0ccec87 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Wed, 22 Oct 2025 11:48:02 +0200 Subject: [PATCH 11/27] Fix test v4.25.0-rc1 --- test/in_command_dependency.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out index 66371d34..e22d70ba 100644 --- a/test/in_command_dependency.expected.out +++ b/test/in_command_dependency.expected.out @@ -11,7 +11,7 @@ {"severity": "info", "pos": {"line": 2, "column": 22}, "endPos": {"line": 2, "column": 28}, - "data": "Try this:\n exact x"}], + "data": "Try this:\n [apply] exact x"}], "env": 0} {"sorries": @@ -40,6 +40,6 @@ [{"severity": "info", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "Try this:\n exact x"}], + "data": "Try this:\n [apply] exact x"}], "goals": []} From 5bc2e03f4720b8b061d4df639bef730d20dc2f20 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:45 +0200 Subject: [PATCH 12/27] Init commit --- REPL/Frontend.lean | 5 ++- REPL/Main.lean | 97 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 98 insertions(+), 4 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index bc2dff1e..4e79fa6b 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -64,6 +64,7 @@ Returns: 3. List of info trees along with Command.State from the incremental processing -/ def processInput (input : String) (cmdState? : Option Command.State) + (incrementalState? : Option IncrementalState := none) (opts : Options := {}) (fileName : Option String := none) : IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do Lean.initSearchPath (← Lean.findSysroot) @@ -76,9 +77,9 @@ def processInput (input : String) (cmdState? : Option Command.State) let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx let headerOnlyState := Command.mkState env messages opts - let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState + let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? return (headerOnlyState, incStates) | some cmdStateBefore => do let parserState : Parser.ModuleParserState := {} - let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore + let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? return (cmdStateBefore, incStates) diff --git a/REPL/Main.lean b/REPL/Main.lean index 078c44b5..08f04416 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -72,7 +72,17 @@ structure State where and report the numerical index for the recorded state at each sorry. -/ proofStates : Array ProofSnapshot := #[] - + /-- + Stores the command text and incremental states for each command, indexed by command ID. + Used for prefix matching to enable incremental processing reuse. + -/ + cmdTexts : Array String := #[] + cmdIncrementalStates : Array (List (IncrementalState × Option InfoTree)) := #[] + /-- + Stores the environment ID that each command was built upon. + Used to ensure prefix matching only considers compatible environment chains. + -/ + cmdEnvChain : Array (Option Nat) := #[] /-- The Lean REPL monad. @@ -88,12 +98,80 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do modify fun s => { s with cmdStates := s.cmdStates.push state } return id +/-- Record command text and incremental states for prefix matching reuse. -/ +def recordCommandIncrementals (cmdText : String) + (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do + modify fun s => { s with + cmdTexts := s.cmdTexts.push cmdText + cmdIncrementalStates := s.cmdIncrementalStates.push incStates + cmdEnvChain := s.cmdEnvChain.push envId? } + /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do let id := (← get).proofStates.size modify fun s => { s with proofStates := s.proofStates.push proofState } return id +/-- Find the longest common prefix between two strings. -/ +def longestCommonPrefix (s1 s2 : String) : Nat := + let chars1 := s1.toList + let chars2 := s2.toList + let rec loop (acc : Nat) : List Char → List Char → Nat + | [], _ => acc + | _, [] => acc + | c1 :: cs1, c2 :: cs2 => + if c1 = c2 then loop (acc + 1) cs1 cs2 else acc + loop 0 chars1 chars2 + +/-- Check if two commands start from the exact same base environment. -/ +def haveSameBaseEnv (envId1? envId2? : Option Nat) : Bool := + match envId1?, envId2? with + | none, none => true -- Both are from fresh environments + | some id1, some id2 => id1 = id2 -- Same environment ID + | _, _ => false -- One fresh, one inherited - different base environments + +/-- Find the best incremental state to reuse based on longest prefix matching from commands with the same base environment. -/ +def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do + let state ← get + if state.cmdTexts.isEmpty then + return none + + -- Find the command with the longest common prefix in the same environment chain + let mut bestPrefix := 0 + let mut bestIncrState : Option IncrementalState := none + + for i in [:state.cmdTexts.size] do + -- Check if this command starts from the same base environment + let cmdEnvId := if i < state.cmdEnvChain.size then state.cmdEnvChain[i]! else none + let hasSameBase := haveSameBaseEnv envId? cmdEnvId + + if hasSameBase then + let cmdText := state.cmdTexts[i]! + let prefixLen := longestCommonPrefix newCmd cmdText + + -- Only consider significant prefixes (at least 10 characters to avoid noise) + if prefixLen > bestPrefix && prefixLen ≥ 10 then + let incStates := state.cmdIncrementalStates[i]! + -- Find the latest incremental state that doesn't exceed our prefix + for (incState, _) in incStates.reverse do + -- Convert string prefix length to byte position for comparison + let prefixBytes := (cmdText.take prefixLen).utf8ByteSize + if incState.cmdPos.byteIdx ≤ prefixBytes then + bestPrefix := prefixLen + bestIncrState := some incState + break + + -- Print debug information about reuse + match bestIncrState with + | some _ => IO.println s!"Found incremental state to reuse (prefix length: {bestPrefix}, env chain compatible)" + | none => + if state.cmdTexts.isEmpty then + IO.println "No previous commands available for reuse" + else + IO.println "No suitable incremental state found for reuse (considering environment chain compatibility)" + + return bestIncrState + def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with @@ -324,11 +402,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState + + -- Find the best incremental state to reuse based on prefix matching + let bestIncrementalState? ← findBestIncrementalState s.cmd s.env + let (initialCmdState, incStates, messages) ← try - IO.processInput s.cmd initialCmdState? + IO.processInput s.cmd initialCmdState? (incrementalState? := bestIncrementalState?) catch ex => return .inr ⟨ex.toString⟩ + -- Store the command text and incremental states for future reuse + recordCommandIncrementals s.cmd incStates s.env + + -- showcase the input string for each incremental state + let mut prevPos := 0 + for (incState, _) in incStates do + let endPos := incState.cmdPos + let processedText := incState.inputCtx.input.extract prevPos endPos + IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n```lean4\n{processedText}\n```" + prevPos := endPos + let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From dc47b431fc48958cd186233b2d4c4eea479b69b6 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 13/27] Implement trie-based prefix matching --- REPL/Frontend.lean | 28 +++++++---- REPL/Main.lean | 115 +++++++++++++++------------------------------ 2 files changed, 57 insertions(+), 86 deletions(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 4e79fa6b..e549a1fa 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import Lean.Elab.Frontend +import Std.Data.HashMap open Lean Elab Language @@ -57,29 +58,40 @@ def processCommandsWithInfoTrees /-- Process some text input, with or without an existing command state. +Supports header caching to avoid reprocessing the same imports repeatedly. Returns: 1. The resulting command state after processing the entire input 2. List of messages 3. List of info trees along with Command.State from the incremental processing +4. Updated header cache mapping import keys to Command.State -/ def processInput (input : String) (cmdState? : Option Command.State) (incrementalState? : Option IncrementalState := none) + (headerCache : Std.HashMap String Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do + IO (Command.State × List (IncrementalState × Option InfoTree) × List Message × (Std.HashMap String Command.State)) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName match cmdState? with | none => do - -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← processHeader header opts messages inputCtx - let headerOnlyState := Command.mkState env messages opts - let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? - return (headerOnlyState, incStates) + let importKey := (input.take parserState.pos.byteIdx).trim + match headerCache.get? importKey with + | some cachedHeaderState => do + -- Header is cached, use it as the base command state + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cachedHeaderState incrementalState? + return (cachedHeaderState, incStates, messages, headerCache) + | none => do + -- Header not cached, process it and cache the result + let (env, messages) ← processHeader header opts messages inputCtx + let headerOnlyState := Command.mkState env messages opts + let headerCache := headerCache.insert importKey headerOnlyState + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState? + return (headerOnlyState, incStates, messages, headerCache) | some cmdStateBefore => do let parserState : Parser.ModuleParserState := {} - let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? - return (cmdStateBefore, incStates) + let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState? + return (cmdStateBefore, incStates, messages, headerCache) diff --git a/REPL/Main.lean b/REPL/Main.lean index 08f04416..523269fa 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,8 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import Lean.Data.Trie +import Std.Data.HashMap /-! # A REPL for Lean. @@ -73,16 +75,16 @@ structure State where -/ proofStates : Array ProofSnapshot := #[] /-- - Stores the command text and incremental states for each command, indexed by command ID. - Used for prefix matching to enable incremental processing reuse. + Trie-based storage for fast prefix matching, organized by environment ID. + Map from environment ID (None for fresh env) to trie of command prefixes with incremental states. -/ - cmdTexts : Array String := #[] - cmdIncrementalStates : Array (List (IncrementalState × Option InfoTree)) := #[] + envTries : Std.HashMap (Option Nat) (Lean.Data.Trie IncrementalState) := Std.HashMap.emptyWithCapacity 8 /-- - Stores the environment ID that each command was built upon. - Used to ensure prefix matching only considers compatible environment chains. + Cache for processed headers (import statements) to avoid reprocessing the same imports repeatedly. + Maps import raw string to the processed command state. -/ - cmdEnvChain : Array (Option Nat) := #[] + headerCache : Std.HashMap String Command.State := Std.HashMap.emptyWithCapacity 8 + /-- The Lean REPL monad. @@ -98,13 +100,24 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do modify fun s => { s with cmdStates := s.cmdStates.push state } return id +/-- Add all incremental states of a command to the trie at their corresponding prefix positions -/ +def addCommandToTrie (cmdText : String) + (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do + let state ← get + let currentTrie := state.envTries.get? envId? |>.getD Lean.Data.Trie.empty + + let mut newTrie := currentTrie + for (incState, _) in incStates do + let prefixPos := incState.cmdPos.byteIdx + let cmdPrefix : String := (cmdText.take prefixPos).trim + newTrie := newTrie.insert cmdPrefix incState + + modify fun s => { s with envTries := s.envTries.insert envId? newTrie } + /-- Record command text and incremental states for prefix matching reuse. -/ def recordCommandIncrementals (cmdText : String) (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do - modify fun s => { s with - cmdTexts := s.cmdTexts.push cmdText - cmdIncrementalStates := s.cmdIncrementalStates.push incStates - cmdEnvChain := s.cmdEnvChain.push envId? } + addCommandToTrie cmdText incStates envId? /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do @@ -112,65 +125,17 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do modify fun s => { s with proofStates := s.proofStates.push proofState } return id -/-- Find the longest common prefix between two strings. -/ -def longestCommonPrefix (s1 s2 : String) : Nat := - let chars1 := s1.toList - let chars2 := s2.toList - let rec loop (acc : Nat) : List Char → List Char → Nat - | [], _ => acc - | _, [] => acc - | c1 :: cs1, c2 :: cs2 => - if c1 = c2 then loop (acc + 1) cs1 cs2 else acc - loop 0 chars1 chars2 - -/-- Check if two commands start from the exact same base environment. -/ -def haveSameBaseEnv (envId1? envId2? : Option Nat) : Bool := - match envId1?, envId2? with - | none, none => true -- Both are from fresh environments - | some id1, some id2 => id1 = id2 -- Same environment ID - | _, _ => false -- One fresh, one inherited - different base environments - -/-- Find the best incremental state to reuse based on longest prefix matching from commands with the same base environment. -/ +/-- Find the best incremental state using trie-based prefix matching -/ def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do let state ← get - if state.cmdTexts.isEmpty then - return none - - -- Find the command with the longest common prefix in the same environment chain - let mut bestPrefix := 0 - let mut bestIncrState : Option IncrementalState := none - - for i in [:state.cmdTexts.size] do - -- Check if this command starts from the same base environment - let cmdEnvId := if i < state.cmdEnvChain.size then state.cmdEnvChain[i]! else none - let hasSameBase := haveSameBaseEnv envId? cmdEnvId - - if hasSameBase then - let cmdText := state.cmdTexts[i]! - let prefixLen := longestCommonPrefix newCmd cmdText - - -- Only consider significant prefixes (at least 10 characters to avoid noise) - if prefixLen > bestPrefix && prefixLen ≥ 10 then - let incStates := state.cmdIncrementalStates[i]! - -- Find the latest incremental state that doesn't exceed our prefix - for (incState, _) in incStates.reverse do - -- Convert string prefix length to byte position for comparison - let prefixBytes := (cmdText.take prefixLen).utf8ByteSize - if incState.cmdPos.byteIdx ≤ prefixBytes then - bestPrefix := prefixLen - bestIncrState := some incState - break - - -- Print debug information about reuse - match bestIncrState with - | some _ => IO.println s!"Found incremental state to reuse (prefix length: {bestPrefix}, env chain compatible)" - | none => - if state.cmdTexts.isEmpty then - IO.println "No previous commands available for reuse" - else - IO.println "No suitable incremental state found for reuse (considering environment chain compatibility)" - - return bestIncrState + let trimmedCmd := newCmd.trim + let trie? := state.envTries.get? envId? + match trie? with + | none => return none + | some trie => + match trie.matchPrefix trimmedCmd 0 with + | some incState => return some incState + | none => return none def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := @@ -406,22 +371,16 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do -- Find the best incremental state to reuse based on prefix matching let bestIncrementalState? ← findBestIncrementalState s.cmd s.env - let (initialCmdState, incStates, messages) ← try - IO.processInput s.cmd initialCmdState? (incrementalState? := bestIncrementalState?) + let (initialCmdState, incStates, messages, headerCache) ← try + IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache catch ex => return .inr ⟨ex.toString⟩ + modify fun st => { st with headerCache := headerCache } + -- Store the command text and incremental states for future reuse recordCommandIncrementals s.cmd incStates s.env - -- showcase the input string for each incremental state - let mut prevPos := 0 - for (incState, _) in incStates do - let endPos := incState.cmdPos - let processedText := incState.inputCtx.input.extract prevPos endPos - IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n```lean4\n{processedText}\n```" - prevPos := endPos - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From b6629a2ef0d3743508330aa656d29c7a9482ef11 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 14/27] Add test example --- test/Mathlib/test/incrementality.expected.out | 68 +++++++++++++++++++ test/Mathlib/test/incrementality.in | 3 + 2 files changed, 71 insertions(+) create mode 100644 test/Mathlib/test/incrementality.expected.out create mode 100644 test/Mathlib/test/incrementality.in diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out new file mode 100644 index 00000000..28cbaee6 --- /dev/null +++ b/test/Mathlib/test/incrementality.expected.out @@ -0,0 +1,68 @@ +{"tactics": + [{"usedConstants": + ["Nat.gcd", + "HMul.hMul", + "Mathlib.Meta.NormNum.isNat_eq_true", + "instMulNat", + "instOfNatNat", + "Mathlib.Meta.NormNum.isNat_ofNat", + "Tactic.NormNum.nat_gcd_helper_2", + "Nat.instAddMonoidWithOne", + "Nat", + "Eq.refl", + "Mathlib.Meta.NormNum.instAddMonoidWithOneNat", + "Tactic.NormNum.isNat_gcd", + "OfNat.ofNat", + "instHMul"], + "tactic": "norm_num", + "proofState": 0, + "pos": {"line": 2, "column": 60}, + "goals": "⊢ Nat.gcd 180 168 = 12", + "endPos": {"line": 2, "column": 68}}, + {"usedConstants": ["Eq.refl"], + "tactic": "rfl", + "proofState": 1, + "pos": {"line": 10, "column": 2}, + "goals": "α✝ : Sort u_1\nn : α✝\n⊢ n = n", + "endPos": {"line": 10, "column": 5}}], + "messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 5}, + "data": "9227465"}], + "env": 0} + +{"tactics": + [{"usedConstants": + ["Nat.gcd", + "HMul.hMul", + "Mathlib.Meta.NormNum.isNat_eq_true", + "instMulNat", + "instOfNatNat", + "Mathlib.Meta.NormNum.isNat_ofNat", + "Tactic.NormNum.nat_gcd_helper_2", + "Nat.instAddMonoidWithOne", + "Nat", + "Eq.refl", + "Mathlib.Meta.NormNum.instAddMonoidWithOneNat", + "Tactic.NormNum.isNat_gcd", + "OfNat.ofNat", + "instHMul"], + "tactic": "norm_num", + "proofState": 2, + "pos": {"line": 2, "column": 60}, + "goals": "⊢ Nat.gcd 180 168 = 12", + "endPos": {"line": 2, "column": 68}}, + {"usedConstants": ["Nat", "Eq.refl"], + "tactic": "rfl", + "proofState": 3, + "pos": {"line": 10, "column": 2}, + "goals": "n : ℕ\n⊢ n = n + 0", + "endPos": {"line": 10, "column": 5}}], + "messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 5}, + "data": "9227465"}], + "env": 1} + diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in new file mode 100644 index 00000000..43e5fb5e --- /dev/null +++ b/test/Mathlib/test/incrementality.in @@ -0,0 +1,3 @@ +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} + +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} From 1af83925b5f7f21c76d276bafbddccdcd8a26fc9 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:46 +0200 Subject: [PATCH 15/27] Fix sensitivity to comments and whitespaces in the header --- REPL/Frontend.lean | 2 +- test/Mathlib/test/incrementality.expected.out | 2 ++ test/Mathlib/test/incrementality.in | 2 ++ 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index e549a1fa..20885db9 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -78,7 +78,7 @@ def processInput (input : String) (cmdState? : Option Command.State) match cmdState? with | none => do let (header, parserState, messages) ← Parser.parseHeader inputCtx - let importKey := (input.take parserState.pos.byteIdx).trim + let importKey := toString header.raw -- do not contain comments and whitespace match headerCache.get? importKey with | some cachedHeaderState => do -- Header is cached, use it as the base command state diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out index 28cbaee6..db70a9b3 100644 --- a/test/Mathlib/test/incrementality.expected.out +++ b/test/Mathlib/test/incrementality.expected.out @@ -66,3 +66,5 @@ "data": "9227465"}], "env": 1} +{"env": 2} + diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in index 43e5fb5e..19bea50e 100644 --- a/test/Mathlib/test/incrementality.in +++ b/test/Mathlib/test/incrementality.in @@ -1,3 +1,5 @@ {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} + +{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"} From 04b2028d59acc5b77367fb4c68987a380bcafc1b Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 16/27] Fix trie stack overflow issue --- REPL/Main.lean | 5 +- REPL/Util/Trie.lean | 146 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 149 insertions(+), 2 deletions(-) create mode 100644 REPL/Util/Trie.lean diff --git a/REPL/Main.lean b/REPL/Main.lean index 523269fa..fb6a5e70 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,7 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import REPL.Util.Trie import Lean.Data.Trie import Std.Data.HashMap @@ -110,7 +111,7 @@ def addCommandToTrie (cmdText : String) for (incState, _) in incStates do let prefixPos := incState.cmdPos.byteIdx let cmdPrefix : String := (cmdText.take prefixPos).trim - newTrie := newTrie.insert cmdPrefix incState + newTrie := REPL.Util.Trie.insert newTrie cmdPrefix incState modify fun s => { s with envTries := s.envTries.insert envId? newTrie } @@ -133,7 +134,7 @@ def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Opti match trie? with | none => return none | some trie => - match trie.matchPrefix trimmedCmd 0 with + match REPL.Util.Trie.matchPrefix trie trimmedCmd 0 with | some incState => return some incState | none => return none diff --git a/REPL/Util/Trie.lean b/REPL/Util/Trie.lean new file mode 100644 index 00000000..b7c6b12f --- /dev/null +++ b/REPL/Util/Trie.lean @@ -0,0 +1,146 @@ +/- +Utilities for working with Lean's string Trie without deep recursion. +We provide iterative insert and matchPrefix to avoid stack overflows for +very long strings (e.g., multi-KB inputs). +-/ + +import Lean.Data.Trie + +namespace REPL.Util.Trie + +open Lean +open Lean.Data + +namespace Internal + +/-- Frames for rebuilding parent nodes after iteratively descending the trie. -/ +inductive Frame (α : Type) where + | node1 (v : Option α) (c : UInt8) : Frame α + | node (v : Option α) (cs : ByteArray) (ts : Array (Lean.Data.Trie α)) (idx : Nat) : Frame α + deriving Inhabited + +end Internal + +/-- Insert or replace the value at key `s` into trie `t` iteratively. -/ +def insert {α} (t : Lean.Data.Trie α) (s : String) (val : α) : Lean.Data.Trie α := + Id.run do + let bytes := s.toUTF8 + let n := bytes.size + + -- Build the suffix path from position `start` to the end of `s`. + let mkSuffixFrom (start : Nat) : Lean.Data.Trie α := + Id.run do + let mut r : Lean.Data.Trie α := Lean.Data.Trie.leaf (some val) + let mut j : Nat := n + while j > start do + let jp := j - 1 + let c := bytes.get! jp + r := Lean.Data.Trie.node1 none c r + j := jp + return r + + -- Descent state + let mut i : Nat := 0 + let mut cur : Lean.Data.Trie α := t + let mut stack : Array (Internal.Frame α) := #[] + + -- Iteratively descend until we either finish the key or need to branch/extend. + let mut done := false + let mut out := cur + while !done do + match cur with + | Lean.Data.Trie.leaf v => + if i < n then + let c := bytes.get! i + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node1 v c suffix + else + out := Lean.Data.Trie.leaf (some val) + done := true + | Lean.Data.Trie.node1 v c' t' => + if i < n then + let c := bytes.get! i + if c == c' then + stack := stack.push (Internal.Frame.node1 v c') + cur := t' + i := i + 1 + else + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node v (ByteArray.mk #[c, c']) (#[(suffix), t']) + done := true + else + out := Lean.Data.Trie.node1 (some val) c' t' + done := true + | Lean.Data.Trie.node v cs ts => + if i < n then + let c := bytes.get! i + match cs.findIdx? (· == c) with + | none => + let suffix := mkSuffixFrom (i + 1) + out := Lean.Data.Trie.node v (cs.push c) (ts.push suffix) + done := true + | some idx => + stack := stack.push (Internal.Frame.node v cs ts idx) + cur := ts[idx]! + i := i + 1 + else + out := Lean.Data.Trie.node (some val) cs ts + done := true + + -- Rebuild parents from the stack + let mut res := out + for frame in stack.reverse do + match frame with + | Internal.Frame.node1 v c => + res := Lean.Data.Trie.node1 v c res + | Internal.Frame.node v cs ts idx => + res := Lean.Data.Trie.node v cs (ts.set! idx res) + return res + +/-- +Find the longest key in the trie that is contained in the given string `s` at position `i`, +and return the associated value, implemented iteratively to avoid stack overflows. + +Note the argument order is `(t s i)` to match usages in `Main.lean`. +-/ +def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos) : Option α := + Id.run do + let bytes := s.toUTF8 + let n := bytes.size + let mut idx : Nat := i.byteIdx + let mut cur : Lean.Data.Trie α := t + let mut best : Option α := none + let mut done := false + while !done do + match cur with + | Lean.Data.Trie.leaf v => + if v.isSome then + return v + else + return best + | Lean.Data.Trie.node1 v c' t' => + if v.isSome then best := v + if idx < n then + let c := bytes.get! idx + if c == c' then + idx := idx + 1 + cur := t' + else + done := true + else + done := true + | Lean.Data.Trie.node v cs ts => + if v.isSome then best := v + if idx < n then + let c := bytes.get! idx + match cs.findIdx? (· == c) with + | some j => + idx := idx + 1 + cur := ts[j]! + | none => + done := true + else + done := true + return best + +end REPL.Util.Trie From f6b9c1d33e701150954efda1997a2f13b00eb471 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 17/27] Make incrementality optional --- REPL/JSON.lean | 1 + REPL/Main.lean | 21 +++++++++++---------- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index fa44e2a8..70a7313f 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -19,6 +19,7 @@ structure CommandOptions where Anything else is ignored. -/ infotree : Option String + incrementality : Option Bool := none -- whether to use incremental mode optimization /-- Run Lean commands. If `env = none`, starts a new session (in which you can use `import`). diff --git a/REPL/Main.lean b/REPL/Main.lean index fb6a5e70..0ccec7d0 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -369,19 +369,20 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - -- Find the best incremental state to reuse based on prefix matching - let bestIncrementalState? ← findBestIncrementalState s.cmd s.env - - let (initialCmdState, incStates, messages, headerCache) ← try - IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache + let (initialCmdState, incStates, messages) ← try + if s.incrementality.getD false then + let bestIncrementalState? ← findBestIncrementalState s.cmd s.env + let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache + -- Store the command text and incremental states for future reuse + modify fun st => { st with headerCache := headerCache } + recordCommandIncrementals s.cmd incStates s.env + pure (initialCmdState, incStates, messages) + else + let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {} + pure (initialCmdState, incStates, messages) catch ex => return .inr ⟨ex.toString⟩ - modify fun st => { st with headerCache := headerCache } - - -- Store the command text and incremental states for future reuse - recordCommandIncrementals s.cmd incStates s.env - let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m let sorries ← sorriesCmd incStates initialCmdState.env none From 759219e40701beb3b97fc23851c2eabf162e68c8 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:30:47 +0200 Subject: [PATCH 18/27] Update incrementality test --- test/Mathlib/test/incrementality.in | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in index 19bea50e..3e5c1738 100644 --- a/test/Mathlib/test/incrementality.in +++ b/test/Mathlib/test/incrementality.in @@ -1,5 +1,5 @@ -{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true} +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n rfl", "allTactics": true, "incrementality": true} -{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true} +{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n | 0 => 0\n | 1 => 1\n | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n rfl", "allTactics": true, "incrementality": true} -{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"} +{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added", "incrementality": true} From 9a415e8d00c273e05056f10bed6b5de06c6a45ca Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Wed, 22 Oct 2025 12:39:46 +0200 Subject: [PATCH 19/27] Fix compilation warning --- REPL/Util/Trie.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/REPL/Util/Trie.lean b/REPL/Util/Trie.lean index b7c6b12f..bf095237 100644 --- a/REPL/Util/Trie.lean +++ b/REPL/Util/Trie.lean @@ -103,7 +103,7 @@ and return the associated value, implemented iteratively to avoid stack overflow Note the argument order is `(t s i)` to match usages in `Main.lean`. -/ -def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos) : Option α := +def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos.Raw) : Option α := Id.run do let bytes := s.toUTF8 let n := bytes.size From 8fb7050ff7437632b93c7d442aaa72961d7a21ef Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:32:57 +0200 Subject: [PATCH 20/27] Add initial code for extracting information about declarations --- REPL/Extract/Declaration.lean | 231 ++++++++ REPL/JSON.lean | 90 ++- REPL/Main.lean | 7 +- test/extract_declaration.expected.out | 787 ++++++++++++++++++++++++++ test/extract_declaration.in | 1 + test/extract_declaration.lean | 73 +++ 6 files changed, 1187 insertions(+), 2 deletions(-) create mode 100644 REPL/Extract/Declaration.lean create mode 100644 test/extract_declaration.expected.out create mode 100644 test/extract_declaration.in create mode 100644 test/extract_declaration.lean diff --git a/REPL/Extract/Declaration.lean b/REPL/Extract/Declaration.lean new file mode 100644 index 00000000..573b9172 --- /dev/null +++ b/REPL/Extract/Declaration.lean @@ -0,0 +1,231 @@ +import REPL.JSON + +open Lean Elab System Parser + +namespace REPL + +/-! Extract information about declarations from info trees +Inspired by +-/ + +/-- See `Lean.Parser.Command.declModifiers` and `Lean.Elab.elabModifiers` -/ +def getModifiers (stx : Syntax) (ctx: ContextInfo): DeclModifiers := + match stx with + | .node _ ``Command.declModifiers args => + { docString := stx[0].getOptional?.map (fun stx => + { content := stx.prettyPrint.pretty, range := stx.toRange ctx }), + visibility := (stx[2].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", + computeKind := (stx[3].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", + recKind := (stx[5].getOptional?.map (·.prettyPrint.pretty.trim)).getD "default", + isUnsafe := !stx[4].isNone, + attributes := stx[1].getArgs.toList.flatMap parseAttributes, } + | _ => {} + where + /-- Parse attribute instances from a Term.attributes syntax node + See `Lean.Parser.Term.attributes`. + -/ + parseAttributes (attrSyntax : Syntax) : List String := + match attrSyntax with + | .node _ ``Term.attributes args => + -- args[0] is "@[", args[1] is the attribute list, args[2] is "]" + if args.size > 1 then + args[1]!.getArgs.toList.flatMap fun inst => + match inst with + | .node _ ``Term.attrInstance _ => [inst.prettyPrint.pretty.trim] + | _ => [] + else [] + | _ => [] + +partial def getIdents (stx : Syntax) : Array Name := + match stx with + | .node _ _ args => args.flatMap getIdents + | .ident _ _ id _ => #[id] + | _ => #[] + +/-- See `Lean.Elab.Term.toBinderViews` -/ +def toBinderViews (stx : Syntax) : Array BinderView := + let k := stx.getKind + if stx.isIdent || k == ``Term.hole then + -- binderIdent + #[{ id := (expandBinderIdent stx), type := mkHole stx, binderInfo := "default" }] + else if k == ``Lean.Parser.Term.explicitBinder then + -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)` + let ids := getBinderIds stx[1] + let type := stx[2] + let optModifier := stx[3] + ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "default" } + else if k == ``Lean.Parser.Term.implicitBinder then + -- `{` binderIdent+ binderType `}` + let ids := getBinderIds stx[1] + let type := stx[2] + ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "implicit" } + else if k == ``Lean.Parser.Term.strictImplicitBinder then + -- `⦃` binderIdent+ binderType `⦄` + let ids := getBinderIds stx[1] + let type := stx[2] + ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "strictImplicit" } + else if k == ``Lean.Parser.Term.instBinder then + -- `[` optIdent type `]` + let id := expandOptIdent stx[1] + let type := stx[2] + #[ { id := id, type := type, binderInfo := "instImplicit" } ] + else + #[] + where + getBinderIds (ids : Syntax) : Array Syntax := + ids.getArgs.map fun (id : Syntax) => + let k := id.getKind + if k == identKind || k == `Lean.Parser.Term.hole then id + else Syntax.missing + expandBinderType (ref : Syntax) (stx : Syntax) : Syntax := + if stx.getNumArgs == 0 then mkHole ref else stx[1] + expandBinderIdent (stx : Syntax) : Syntax := + match stx with + | `(_) => Syntax.missing + | _ => stx + expandOptIdent (stx : Syntax) : Syntax := + if stx.isNone then Syntax.missing else stx[0] + +def getScope (ctx : ContextInfo) (state : Command.State) : ScopeInfo := + let scope := state.scopes.head! + { + varDecls := scope.varDecls.map fun stx => s!"variable {stx.raw.prettyPrint.pretty}", + includeVars := scope.includedVars.toArray.map fun name => name.eraseMacroScopes, + omitVars := scope.omittedVars.toArray.map fun name => name.eraseMacroScopes, + levelNames := scope.levelNames.toArray, + currNamespace := ctx.currNamespace, + openDecl := ctx.openDecls, + } + +partial def extractDeclarationInfo (cmdInfo : CommandInfo) (infoTree : InfoTree) (ctx : ContextInfo) + (prevState : Command.State) : DeclarationInfo := + let stx := cmdInfo.stx + let modifiers := getModifiers stx[0] ctx + let decl := stx[1] + let kind := decl.getKind + let kindStr := match kind with + | .str _ s => s + | _ => kind.toString + + -- See `Lean.Elab.DefView` + let (signature, id, binders, type?, value?) := match kind with + | ``Command.abbrev + | ``Command.definition => + let (binders, type) := expandOptDeclSig decl[2] + (decl[2], decl[1], binders, type, some decl[3]) + | ``Command.theorem => + let (binders, type) := expandDeclSig decl[2] + (decl[2], decl[1], binders, some type, some decl[3]) + | ``Command.opaque => + let (binders, type) := expandDeclSig decl[2] + (decl[2], decl[1], binders, some type, decl[3].getOptional?) + | ``Command.axiom => + let (binders, type) := expandDeclSig decl[2] + (decl[2], decl[1], binders, some type, none) + | ``Command.inductive + | ``Command.classInductive => + let (binders, type) := expandOptDeclSig decl[2] + (decl[2], decl[1], binders, type, some decl[4]) + | ``Command.instance => + let (binders, type) := expandDeclSig decl[4] + let declId := match stx[3].getOptional? with + | some declId => declId + | none => Syntax.missing -- TODO: improve this + (decl[4], declId, binders, some type, some decl[5]) + | ``Command.example => + let id := mkIdentFrom stx[0] `_example (canonical := true) + let declId := mkNode ``Parser.Command.declId #[id, mkNullNode] + let (binders, type) := expandOptDeclSig decl[1] + (decl[1], declId, binders, type, some decl[2]) + | ``Command.structure => + let signature := Syntax.node2 .none ``Command.optDeclSig decl[2] decl[4] + let (binders, type) := (decl[2], some decl[4]) + (signature, decl[1], binders, type, none) + | _ => unreachable! + + let name := id[0].getId + let fullName := match getFullname infoTree name with -- TODO: could be better + | [] => name + | a :: _ => a + + let binderViews := binders.getArgs.flatMap toBinderViews + let binders : Option DeclBinders := match binders.getArgs with + | #[] => none + | _ => some { pp := binders.prettyPrint.pretty, + groups := binders.getArgs.map (·.prettyPrint.pretty), + map := binders.getArgs.flatMap toBinderViews, + range := binders.toRange ctx } + + let a := prevState.env.constants.find! decl[1].getId + -- a.getUsedConstantsAsSet + + let extractConstants (stx : Syntax) : Array Name := -- TODO: improve this + let idents := ((getIdents stx).foldl + (init := NameSet.empty) fun acc name => acc.insert name).toArray + idents + -- idents.filter prevState.env.constants.contains + + { + pp := stx.prettyPrint.pretty, + name, + fullName, + kind := kindStr, + modifiers, + scope := getScope ctx prevState, + signature := { pp := signature.prettyPrint.pretty, + constants := extractConstants signature, + range := signature.toRange ctx }, + binders, + type := type?.map fun t => + { pp := t.prettyPrint.pretty, constants := extractConstants t, range := t.toRange ctx }, + value := value?.map fun v => + { pp := v.prettyPrint.pretty, constants := extractConstants v, range := v.toRange ctx }, + range := stx.toRange ctx + } +where + getFullname (infoTree : InfoTree) (shortName : Name) : List Name := + match infoTree with + | .context _ t => getFullname t shortName + | .node i ts => + match i with + | .ofTermInfo ti => ti.expr.constName?.toList.filter (fun n => + match shortName.componentsRev with + | [] => true + | h :: _ => match n.componentsRev with + | [] => false + | h' :: _ => h == h' + ) + | _ => ts.toList.flatMap (getFullname · shortName) + | _ => [] + +open Lean.Parser in +/-- Extract all declarations from InfoTrees -/ +partial def extractCmdDeclarationInfos (trees : List InfoTree) (prevState : Command.State) : + List DeclarationInfo := + let allDecls := trees.map (extractFromTree · none prevState) + allDecls.flatten +where + extractFromTree (t : InfoTree) (ctx? : Option ContextInfo) (prevState : Command.State) : + List DeclarationInfo := + match t with + | .context ctx t => extractFromTree t (ctx.mergeIntoOuter? ctx?) prevState + | .node i ts => + match i with + | .ofCommandInfo cmdInfo => + match ctx? with + | some ctx => + if cmdInfo.stx.getKind == ``Command.declaration then + [extractDeclarationInfo cmdInfo t ctx prevState] + else + ts.toList.flatMap (extractFromTree · ctx? prevState) + | none => ts.toList.flatMap (extractFromTree · ctx? prevState) + | _ => ts.toList.flatMap (extractFromTree · ctx? prevState) + | _ => [] + +def extractAllDeclarationInfos (treeList : List (IncrementalState × Option InfoTree)) (prevState : Command.State) : List DeclarationInfo := + match treeList with + | [] => [] + | (state, infoTree?) :: rest => + let decls := extractCmdDeclarationInfos infoTree?.toList prevState + let restDecls := extractAllDeclarationInfos rest state.commandState + decls ++ restDecls diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 70a7313f..db41d579 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import Lean.Data.Json import Lean.Message import Lean.Elab.InfoTree.Main +import REPL.Lean.InfoTree.ToJson open Lean Elab InfoTree @@ -13,6 +14,7 @@ namespace REPL structure CommandOptions where allTactics : Option Bool := none + declarations: Option Bool := none rootGoals : Option Bool := none /-- Should be "full", "tactics", "original", or "substantive". @@ -118,6 +120,91 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : proofState, usedConstants } +structure DocString where + content : String + range : Syntax.Range +deriving ToJson + +/-- See `Lean.Elab.Modifiers` -/ +structure DeclModifiers where + docString : Option DocString := none + visibility : String := "regular" -- "regular", "private", "protected", or "public" + computeKind : String := "regular" -- "regular", "meta", or "noncomputable" + recKind : String := "default" -- "default", "partial", or "nonrec" + isUnsafe : Bool := false + attributes : List String := [] +deriving ToJson + +structure DeclSignature where + pp : String + constants : Array Name + range : Syntax.Range +deriving ToJson + +structure BinderView where + id : Syntax + type : Syntax + binderInfo : String + +instance : ToJson BinderView where + toJson (bv : BinderView) : Json := + Json.mkObj [ + ("id", toString bv.id.prettyPrint), + ("type", toString bv.type.prettyPrint), + ("binderInfo", bv.binderInfo) + ] + +structure DeclBinders where + pp : String + groups : Array String + map : Array BinderView + range : Syntax.Range +deriving ToJson + +structure DeclType where + pp : String + constants : Array Name + range : Syntax.Range +deriving ToJson + +structure DeclValue where + pp : String + constants : Array Name + range : Syntax.Range +deriving ToJson + +local instance : ToJson OpenDecl where + toJson + | .simple ns except => json%{ + simple: { «namespace»: $ns, except: $except } + } + | .explicit id declName => json%{ + rename: { name: $declName, as: $id } + } + +structure ScopeInfo where + varDecls : Array String + includeVars : Array Name + omitVars : Array Name + levelNames : Array Name + currNamespace : Name + openDecl : List OpenDecl +deriving ToJson + +structure DeclarationInfo where + pp: String + range : Syntax.Range + scope : ScopeInfo + name : Name + fullName : Name + kind : String + modifiers : DeclModifiers + signature: DeclSignature + binders : Option DeclBinders := none + type : Option DeclType := none + value : Option DeclValue := none +deriving ToJson + /-- A response to a Lean command. `env` can be used in later calls, to build on the stored environment. @@ -127,8 +214,8 @@ structure CommandResponse where messages : List Message := [] sorries : List Sorry := [] tactics : List Tactic := [] + declarations: List DeclarationInfo := [] infotree : Option Json := none -deriving FromJson def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json) | [] => [] @@ -140,6 +227,7 @@ instance : ToJson CommandResponse where Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "tactics" r.tactics, + Json.nonemptyList "declarations" r.declarations, match r.infotree with | some j => [("infotree", j)] | none => [] ] diff --git a/REPL/Main.lean b/REPL/Main.lean index 0ccec7d0..ff4422f4 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import REPL.JSON import REPL.Frontend import REPL.Util.Path +import REPL.Extract.Declaration import REPL.Lean.ContextInfo import REPL.Lean.Environment import REPL.Lean.InfoTree @@ -392,6 +393,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let tactics ← match s.allTactics with | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] + let declarations := match s.declarations with + | some true => extractAllDeclarationInfos incStates initialCmdState + | _ => [] let cmdSnapshot := { cmdState cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD @@ -417,7 +421,8 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do { env, messages, sorries, - tactics + tactics, + declarations, infotree } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do diff --git a/test/extract_declaration.expected.out b/test/extract_declaration.expected.out new file mode 100644 index 00000000..9a374e9c --- /dev/null +++ b/test/extract_declaration.expected.out @@ -0,0 +1,787 @@ +{"env": 0, + "declarations": + [{"value": + {"range": + {"synthetic": false, + "start": {"line": 6, "column": 20}, + "finish": {"line": 7, "column": 25}}, + "pp": ":=\n println \"Hello, world!\"", + "constants": ["println"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 6, "column": 12}, + "finish": {"line": 6, "column": 19}}, + "pp": "IO Unit", + "constants": ["IO", "Unit"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 6, "column": 10}, + "finish": {"line": 6, "column": 19}}, + "pp": ": IO Unit", + "constants": ["IO", "Unit"]}, + "scope": + {"varDecls": [], + "openDecl": [{"simple": {"namespace": "IO", "except": []}}], + "omitVars": [], + "levelNames": [], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 6, "column": 0}, + "finish": {"line": 7, "column": 25}}, + "pp": "def hello : IO Unit :=\n println \"Hello, world!\"", + "name": "hello", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "hello", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 12, "column": 57}, + "finish": {"line": 14, "column": 13}}, + "pp": ":= by\n intro h₁ h₂\n rw [h₁, h₂]", + "constants": ["h₂", "h₁"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 12, "column": 35}, + "finish": {"line": 12, "column": 56}}, + "pp": "a = b → b = c → c = a", + "constants": ["c", "a", "b"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 12, "column": 21}, + "finish": {"line": 12, "column": 56}}, + "pp": "{a b c : α} : a = b → b = c → c = a", + "constants": ["c", "α", "a", "b"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 12, "column": 0}, + "finish": {"line": 14, "column": 13}}, + "pp": + "theorem eq_trans_sym {a b c : α} : a = b → b = c → c = a := by\n intro h₁ h₂\n rw [h₁, h₂]", + "name": "eq_trans_sym", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "theorem", + "fullName": "eq_trans_sym", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 12, "column": 21}, + "finish": {"line": 12, "column": 32}}, + "pp": "{a b c : α}", + "map": + [{"type": "α", "id": "a", "binderInfo": "implicit"}, + {"type": "α", "id": "b", "binderInfo": "implicit"}, + {"type": "α", "id": "c", "binderInfo": "implicit"}], + "groups": ["{a b c : α}"]}}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 19, "column": 2}, + "finish": {"line": 20, "column": 27}}, + "pp": "| .zero => x\n | .succ n => pow' x n * x", + "constants": ["pow'", "succ", "n", "x", "zero"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 18, "column": 27}, + "finish": {"line": 18, "column": 34}}, + "pp": "Nat → α", + "constants": ["α", "Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 18, "column": 9}, + "finish": {"line": 18, "column": 34}}, + "pp": "[Mul α] (x : α) : Nat → α", + "constants": ["α", "Mul", "Nat", "x"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 16, "column": 0}, + "finish": {"line": 20, "column": 27}}, + "pp": + "/-- Docstring test\npow' x n = x ^ (n + 1) -/\ndef pow' [Mul α] (x : α) : Nat → α\n | .zero => x\n | .succ n => pow' x n * x", + "name": "pow'", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": + {"range": + {"synthetic": false, + "start": {"line": 16, "column": 0}, + "finish": {"line": 17, "column": 25}}, + "content": "/-- Docstring test\npow' x n = x ^ (n + 1) -/"}, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "pow'", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 18, "column": 9}, + "finish": {"line": 18, "column": 24}}, + "pp": "[Mul α] (x : α)", + "map": + [{"type": "Mul α", "id": "", "binderInfo": "instImplicit"}, + {"type": "α", "id": "x", "binderInfo": "default"}], + "groups": ["[Mul α]", "(x : α)"]}}, + {"value": null, + "type": + {"range": + {"synthetic": false, + "start": {"line": 22, "column": 40}, + "finish": {"line": 26, "column": 29}}, + "pp": + "where\n x : Nat\n y : Nat\n z : Nat\n eqn : x ^ k + y ^ k = z ^ k", + "constants": ["eqn", "z", "y", "Nat", "k", "x"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 22, "column": 23}, + "finish": {"line": 26, "column": 29}}, + "pp": + "(k : Nat) : Type where\n x : Nat\n y : Nat\n z : Nat\n eqn : x ^ k + y ^ k = z ^ k", + "constants": ["eqn", "z", "y", "Nat", "k", "x"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 22, "column": 0}, + "finish": {"line": 26, "column": 29}}, + "pp": + "structure FermatTriple (k : Nat) : Type where\n x : Nat\n y : Nat\n z : Nat\n eqn : x ^ k + y ^ k = z ^ k", + "name": "FermatTriple", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "structure", + "fullName": "FermatTriple", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 22, "column": 23}, + "finish": {"line": 22, "column": 39}}, + "pp": "(k : Nat) : Type", + "map": [], + "groups": ["(k : Nat)", ": Type"]}}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 28, "column": 25}, + "finish": {"line": 28, "column": 44}}, + "pp": ":= ⟨ 3, 4, 5, rfl ⟩", + "constants": ["rfl"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 28, "column": 10}, + "finish": {"line": 28, "column": 24}}, + "pp": "FermatTriple 2", + "constants": ["FermatTriple"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 28, "column": 8}, + "finish": {"line": 28, "column": 24}}, + "pp": ": FermatTriple 2", + "constants": ["FermatTriple"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 28, "column": 0}, + "finish": {"line": 28, "column": 44}}, + "pp": "example : FermatTriple 2 := ⟨ 3, 4, 5, rfl ⟩", + "name": "_example", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "example", + "fullName": "_example", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 33, "column": 2}, + "finish": {"line": 33, "column": 7}}, + "pp": "| val", + "constants": ["val"]}, + "type": null, + "signature": + {"range": + {"synthetic": true, + "start": {"line": 1, "column": 0}, + "finish": {"line": 1, "column": 0}}, + "pp": "", + "constants": []}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Demo"}, + "range": + {"synthetic": false, + "start": {"line": 32, "column": 0}, + "finish": {"line": 33, "column": 7}}, + "pp": "inductive MyType\n | val", + "name": "MyType", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "inductive", + "fullName": "Demo.MyType", + "binders": null}, + {"value": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", + "constants": + ["ParserDescr.symbol._@._hyg.226", + "ParserDescr.binary._@._hyg.226", + "ParserDescr.cat._@._hyg.226", + "ParserDescr.trailingNode._@._hyg.226"]}, + "type": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " Lean.TrailingParserDescr ", + "constants": ["Lean.TrailingParserDescr._@._hyg.226"]}, + "signature": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " : Lean.TrailingParserDescr ", + "constants": ["Lean.TrailingParserDescr._@._hyg.226"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Demo"}, + "range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " @[ scoped term_parser 1000 ] meta def «term_≋_» : Lean.TrailingParserDescr := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", + "name": "«term_≋_»", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "meta", + "attributes": ["scoped term_parser 1000"]}, + "kind": "definition", + "fullName": "Demo.«term_≋_»", + "binders": null}, + {"value": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", + "constants": + ["Lean.Macro.Exception.unsupportedSyntax._@._hyg.255", + "throw._@._hyg.255", + "rhs._@._hyg.223", + "BEq.beq", + "lhs._@._hyg.223"]}, + "type": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " Macro ", + "constants": ["Macro._@._hyg.255"]}, + "signature": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " : Macro ", + "constants": ["Macro._@._hyg.255"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Demo"}, + "range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " @[ macro Demo.«term_≋_» ] meta def «_aux___macroRules_Demo_term_≋__1» : Macro := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", + "name": "«_aux___macroRules_Demo_term_≋__1»", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "meta", + "attributes": ["macro Demo.«term_≋_»"]}, + "kind": "definition", + "fullName": "Demo.«_aux___macroRules_Demo_term_≋__1»", + "binders": null}, + {"value": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", + "constants": + ["throw._@._hyg.225", + "rhs._@._hyg.223", + "lhs._@._hyg.223", + "f._@._hyg.225", + "withRef._@._hyg.225"]}, + "type": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " Lean.PrettyPrinter.Unexpander ", + "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]}, + "signature": + {"range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": " : Lean.PrettyPrinter.Unexpander ", + "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Demo"}, + "range": + {"synthetic": true, + "start": {"line": 35, "column": 0}, + "finish": {"line": 35, "column": 32}}, + "pp": + " @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", + "name": "_aux___unexpand_BEq_beq_1", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "meta", + "attributes": ["scoped app_unexpander BEq.beq"]}, + "kind": "definition", + "fullName": "Demo._aux___unexpand_BEq_beq_1", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 37, "column": 29}, + "finish": {"line": 38, "column": 17}}, + "pp": "where\n beq _ _ := true", + "constants": ["beq", "true"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 37, "column": 18}, + "finish": {"line": 37, "column": 28}}, + "pp": "BEq MyType", + "constants": ["MyType", "BEq"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 37, "column": 16}, + "finish": {"line": 37, "column": 28}}, + "pp": ": BEq MyType", + "constants": ["MyType", "BEq"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Demo"}, + "range": + {"synthetic": false, + "start": {"line": 37, "column": 0}, + "finish": {"line": 38, "column": 17}}, + "pp": "scoped instance : BEq MyType where\n beq _ _ := true", + "name": "[anonymous]", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "instance", + "fullName": "Demo.instBEqMyType", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 47, "column": 32}, + "finish": {"line": 53, "column": 38}}, + "pp": + ":= do\n let x : Demo.MyType := Demo.MyType.val\n let y : Demo.MyType := Demo.MyType.val\n if x ≋ y then\n IO.println \"x and y are equal\"\n else\n IO.println \"x and y are not equal\"", + "constants": ["IO.println", "Demo.MyType.val", "y", "Demo.MyType", "x"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 47, "column": 24}, + "finish": {"line": 47, "column": 31}}, + "pp": "IO Unit", + "constants": ["IO", "Unit"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 47, "column": 22}, + "finish": {"line": 47, "column": 31}}, + "pp": ": IO Unit", + "constants": ["IO", "Unit"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 47, "column": 0}, + "finish": {"line": 53, "column": 38}}, + "pp": + "def open_scoped_test1 : IO Unit := do\n let x : Demo.MyType := Demo.MyType.val\n let y : Demo.MyType := Demo.MyType.val\n if x ≋ y then\n IO.println \"x and y are equal\"\n else\n IO.println \"x and y are not equal\"", + "name": "open_scoped_test1", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "open_scoped_test1", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 58, "column": 41}, + "finish": {"line": 59, "column": 7}}, + "pp": ":=\n a * a", + "constants": ["a"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 58, "column": 37}, + "finish": {"line": 58, "column": 40}}, + "pp": "Nat", + "constants": ["Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 58, "column": 25}, + "finish": {"line": 58, "column": 40}}, + "pp": "(a : Nat) : Nat", + "constants": ["a", "Nat"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 58, "column": 0}, + "finish": {"line": 59, "column": 7}}, + "pp": "private def private_test (a : Nat) : Nat :=\n a * a", + "name": "private_test", + "modifiers": + {"visibility": "private", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "_private.0.private_test", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 58, "column": 25}, + "finish": {"line": 58, "column": 34}}, + "pp": "(a : Nat)", + "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}], + "groups": ["(a : Nat)"]}}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 61, "column": 62}, + "finish": {"line": 61, "column": 66}}, + "pp": ":= a", + "constants": ["a"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 61, "column": 58}, + "finish": {"line": 61, "column": 61}}, + "pp": "Nat", + "constants": ["Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 61, "column": 46}, + "finish": {"line": 61, "column": 61}}, + "pp": "(a : Nat) : Nat", + "constants": ["a", "Nat"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 61, "column": 0}, + "finish": {"line": 61, "column": 66}}, + "pp": "private noncomputable def non_computable_test (a : Nat) : Nat := a", + "name": "non_computable_test", + "modifiers": + {"visibility": "private", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "noncomputable", + "attributes": []}, + "kind": "definition", + "fullName": "_private.0.non_computable_test", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 61, "column": 46}, + "finish": {"line": 61, "column": 55}}, + "pp": "(a : Nat)", + "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}], + "groups": ["(a : Nat)"]}}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 66, "column": 52}, + "finish": {"line": 66, "column": 56}}, + "pp": ":= a", + "constants": ["a"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 66, "column": 48}, + "finish": {"line": 66, "column": 51}}, + "pp": "Nat", + "constants": ["Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 66, "column": 36}, + "finish": {"line": 66, "column": 51}}, + "pp": "(a : Nat) : Nat", + "constants": ["a", "Nat"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "Example"}, + "range": + {"synthetic": false, + "start": {"line": 64, "column": 0}, + "finish": {"line": 66, "column": 56}}, + "pp": + "/--\n dododo-/\nprotected partial def prot_part_def (a : Nat) : Nat := a", + "name": "prot_part_def", + "modifiers": + {"visibility": "protected", + "recKind": "partial", + "isUnsafe": false, + "docString": + {"range": + {"synthetic": false, + "start": {"line": 64, "column": 0}, + "finish": {"line": 65, "column": 9}}, + "content": "/--\n dododo-/"}, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "Example.prot_part_def", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 66, "column": 36}, + "finish": {"line": 66, "column": 45}}, + "pp": "(a : Nat)", + "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}], + "groups": ["(a : Nat)"]}}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 69, "column": 30}, + "finish": {"line": 69, "column": 35}}, + "pp": ":= 42", + "constants": []}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 69, "column": 26}, + "finish": {"line": 69, "column": 29}}, + "pp": "Nat", + "constants": ["Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 69, "column": 24}, + "finish": {"line": 69, "column": 29}}, + "pp": ": Nat", + "constants": ["Nat"]}, + "scope": + {"varDecls": ["variable {α : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 69, "column": 0}, + "finish": {"line": 69, "column": 35}}, + "pp": "@[simp, instance] def t : Nat := 42", + "name": "t", + "modifiers": + {"visibility": "regular", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": ["simp", "instance"]}, + "kind": "definition", + "fullName": "t", + "binders": null}, + {"value": + {"range": + {"synthetic": false, + "start": {"line": 72, "column": 39}, + "finish": {"line": 73, "column": 7}}, + "pp": ":=\n a + t", + "constants": ["t", "a"]}, + "type": + {"range": + {"synthetic": false, + "start": {"line": 72, "column": 35}, + "finish": {"line": 72, "column": 38}}, + "pp": "Nat", + "constants": ["Nat"]}, + "signature": + {"range": + {"synthetic": false, + "start": {"line": 72, "column": 23}, + "finish": {"line": 72, "column": 38}}, + "pp": "(a : Nat) : Nat", + "constants": ["a", "Nat"]}, + "scope": + {"varDecls": ["variable {α : Type u}", "variable {β : Type u}"], + "openDecl": [], + "omitVars": [], + "levelNames": ["u"], + "includeVars": [], + "currNamespace": "[anonymous]"}, + "range": + {"synthetic": false, + "start": {"line": 72, "column": 0}, + "finish": {"line": 73, "column": 7}}, + "pp": "public def public_test (a : Nat) : Nat :=\n a + t", + "name": "public_test", + "modifiers": + {"visibility": "public", + "recKind": "default", + "isUnsafe": false, + "docString": null, + "computeKind": "regular", + "attributes": []}, + "kind": "definition", + "fullName": "public_test", + "binders": + {"range": + {"synthetic": false, + "start": {"line": 72, "column": 23}, + "finish": {"line": 72, "column": 32}}, + "pp": "(a : Nat)", + "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}], + "groups": ["(a : Nat)"]}}]} + diff --git a/test/extract_declaration.in b/test/extract_declaration.in new file mode 100644 index 00000000..ee592337 --- /dev/null +++ b/test/extract_declaration.in @@ -0,0 +1 @@ +{"path": "test/extract_declaration.lean", "declarations": true} diff --git a/test/extract_declaration.lean b/test/extract_declaration.lean new file mode 100644 index 00000000..586e1f74 --- /dev/null +++ b/test/extract_declaration.lean @@ -0,0 +1,73 @@ +import Lean + +/-! Inspired by Jixia examples -/ + +open IO in +def hello : IO Unit := + println "Hello, world!" + +universe u +variable {α : Type u} + +theorem eq_trans_sym {a b c : α} : a = b → b = c → c = a := by + intro h₁ h₂ + rw [h₁, h₂] + +/-- Docstring test +pow' x n = x ^ (n + 1) -/ +def pow' [Mul α] (x : α) : Nat → α + | .zero => x + | .succ n => pow' x n * x + +structure FermatTriple (k : Nat) : Type where + x : Nat + y : Nat + z : Nat + eqn : x ^ k + y ^ k = z ^ k + +example : FermatTriple 2 := ⟨ 3, 4, 5, rfl ⟩ + +namespace Demo + +inductive MyType + | val + +scoped infix:68 " ≋ " => BEq.beq + +scoped instance : BEq MyType where + beq _ _ := true + +end Demo + + +section + +open scoped Demo + +def open_scoped_test1 : IO Unit := do + let x : Demo.MyType := Demo.MyType.val + let y : Demo.MyType := Demo.MyType.val + if x ≋ y then + IO.println "x and y are equal" + else + IO.println "x and y are not equal" +end + +section + +private def private_test (a : Nat) : Nat := + a * a + +private noncomputable def non_computable_test (a : Nat) : Nat := a + +namespace Example +/-- + dododo-/ +protected partial def prot_part_def (a : Nat) : Nat := a +end Example + +@[simp, instance] def t : Nat := 42 + +variable {β : Type u} +public def public_test (a : Nat) : Nat := + a + t From a5019291ccee58e9b9486e5fe25d8109887cc1f8 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:32:57 +0200 Subject: [PATCH 21/27] Clean unused variables --- REPL/Extract/Declaration.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/REPL/Extract/Declaration.lean b/REPL/Extract/Declaration.lean index 573b9172..aa13ee16 100644 --- a/REPL/Extract/Declaration.lean +++ b/REPL/Extract/Declaration.lean @@ -11,7 +11,7 @@ Inspired by /-- See `Lean.Parser.Command.declModifiers` and `Lean.Elab.elabModifiers` -/ def getModifiers (stx : Syntax) (ctx: ContextInfo): DeclModifiers := match stx with - | .node _ ``Command.declModifiers args => + | .node _ ``Command.declModifiers _ => { docString := stx[0].getOptional?.map (fun stx => { content := stx.prettyPrint.pretty, range := stx.toRange ctx }), visibility := (stx[2].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", @@ -52,7 +52,7 @@ def toBinderViews (stx : Syntax) : Array BinderView := -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)` let ids := getBinderIds stx[1] let type := stx[2] - let optModifier := stx[3] + -- let optModifier := stx[3] ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "default" } else if k == ``Lean.Parser.Term.implicitBinder then -- `{` binderIdent+ binderType `}` @@ -148,7 +148,6 @@ partial def extractDeclarationInfo (cmdInfo : CommandInfo) (infoTree : InfoTree) | [] => name | a :: _ => a - let binderViews := binders.getArgs.flatMap toBinderViews let binders : Option DeclBinders := match binders.getArgs with | #[] => none | _ => some { pp := binders.prettyPrint.pretty, @@ -156,7 +155,7 @@ partial def extractDeclarationInfo (cmdInfo : CommandInfo) (infoTree : InfoTree) map := binders.getArgs.flatMap toBinderViews, range := binders.toRange ctx } - let a := prevState.env.constants.find! decl[1].getId + -- let a := prevState.env.constants.find! decl[1].getId -- a.getUsedConstantsAsSet let extractConstants (stx : Syntax) : Array Name := -- TODO: improve this From 13e3ae4aeda0828213c369d62070983660707b30 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:32:57 +0200 Subject: [PATCH 22/27] Update `protected` extraction status to match v4.23.0 change --- REPL/Extract/Declaration.lean | 7 +-- REPL/JSON.lean | 3 +- test/extract_declaration.expected.out | 61 +++++++++++++++++---------- 3 files changed, 45 insertions(+), 26 deletions(-) diff --git a/REPL/Extract/Declaration.lean b/REPL/Extract/Declaration.lean index aa13ee16..c1d3c973 100644 --- a/REPL/Extract/Declaration.lean +++ b/REPL/Extract/Declaration.lean @@ -15,9 +15,10 @@ def getModifiers (stx : Syntax) (ctx: ContextInfo): DeclModifiers := { docString := stx[0].getOptional?.map (fun stx => { content := stx.prettyPrint.pretty, range := stx.toRange ctx }), visibility := (stx[2].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", - computeKind := (stx[3].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", - recKind := (stx[5].getOptional?.map (·.prettyPrint.pretty.trim)).getD "default", - isUnsafe := !stx[4].isNone, + computeKind := (stx[4].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular", + isProtected := !stx[3].isNone, + isUnsafe := !stx[5].isNone, + recKind := (stx[6].getOptional?.map (·.prettyPrint.pretty.trim)).getD "default", attributes := stx[1].getArgs.toList.flatMap parseAttributes, } | _ => {} where diff --git a/REPL/JSON.lean b/REPL/JSON.lean index db41d579..3cfdaaaf 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -128,9 +128,10 @@ deriving ToJson /-- See `Lean.Elab.Modifiers` -/ structure DeclModifiers where docString : Option DocString := none - visibility : String := "regular" -- "regular", "private", "protected", or "public" + visibility : String := "regular" -- "regular", "private", or "public" computeKind : String := "regular" -- "regular", "meta", or "noncomputable" recKind : String := "default" -- "default", "partial", or "nonrec" + isProtected : Bool := false isUnsafe : Bool := false attributes : List String := [] deriving ToJson diff --git a/test/extract_declaration.expected.out b/test/extract_declaration.expected.out index 9a374e9c..23458139 100644 --- a/test/extract_declaration.expected.out +++ b/test/extract_declaration.expected.out @@ -38,6 +38,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -83,6 +84,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -138,6 +140,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": {"range": {"synthetic": false, @@ -193,6 +196,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -244,6 +248,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -282,6 +287,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -296,24 +302,24 @@ "pp": " := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", "constants": - ["ParserDescr.symbol._@._hyg.226", - "ParserDescr.binary._@._hyg.226", - "ParserDescr.cat._@._hyg.226", - "ParserDescr.trailingNode._@._hyg.226"]}, + ["ParserDescr.cat._@._hyg.202", + "ParserDescr.symbol._@._hyg.202", + "ParserDescr.binary._@._hyg.202", + "ParserDescr.trailingNode._@._hyg.202"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Lean.TrailingParserDescr ", - "constants": ["Lean.TrailingParserDescr._@._hyg.226"]}, + "constants": ["Lean.TrailingParserDescr._@._hyg.202"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Lean.TrailingParserDescr ", - "constants": ["Lean.TrailingParserDescr._@._hyg.226"]}, + "constants": ["Lean.TrailingParserDescr._@._hyg.202"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -332,6 +338,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "meta", "attributes": ["scoped term_parser 1000"]}, @@ -346,25 +353,25 @@ "pp": " := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", "constants": - ["Lean.Macro.Exception.unsupportedSyntax._@._hyg.255", - "throw._@._hyg.255", - "rhs._@._hyg.223", + ["rhs._@._hyg.199", + "throw._@._hyg.221", + "Lean.Macro.Exception.unsupportedSyntax._@._hyg.221", "BEq.beq", - "lhs._@._hyg.223"]}, + "lhs._@._hyg.199"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Macro ", - "constants": ["Macro._@._hyg.255"]}, + "constants": ["Macro._@._hyg.221"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Macro ", - "constants": ["Macro._@._hyg.255"]}, + "constants": ["Macro._@._hyg.221"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -383,6 +390,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "meta", "attributes": ["macro Demo.«term_≋_»"]}, @@ -395,27 +403,28 @@ "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": - " := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", + " := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", "constants": - ["throw._@._hyg.225", - "rhs._@._hyg.223", - "lhs._@._hyg.223", - "f._@._hyg.225", - "withRef._@._hyg.225"]}, + ["rhs._@._hyg.199", + "throw._@._hyg.201", + "_@._hyg.201", + "withRef._@._hyg.201", + "f._@._hyg.201", + "lhs._@._hyg.199"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Lean.PrettyPrinter.Unexpander ", - "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]}, + "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Lean.PrettyPrinter.Unexpander ", - "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]}, + "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -428,12 +437,13 @@ "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": - " @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", + " @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", "name": "_aux___unexpand_BEq_beq_1", "modifiers": {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "meta", "attributes": ["scoped app_unexpander BEq.beq"]}, @@ -478,6 +488,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -524,6 +535,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -568,6 +580,7 @@ {"visibility": "private", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, @@ -619,6 +632,7 @@ {"visibility": "private", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "noncomputable", "attributes": []}, @@ -668,9 +682,10 @@ "/--\n dododo-/\nprotected partial def prot_part_def (a : Nat) : Nat := a", "name": "prot_part_def", "modifiers": - {"visibility": "protected", + {"visibility": "regular", "recKind": "partial", "isUnsafe": false, + "isProtected": true, "docString": {"range": {"synthetic": false, @@ -727,6 +742,7 @@ {"visibility": "regular", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": ["simp", "instance"]}, @@ -771,6 +787,7 @@ {"visibility": "public", "recKind": "default", "isUnsafe": false, + "isProtected": false, "docString": null, "computeKind": "regular", "attributes": []}, From 5888586088b8f915c60f262c8468ce0153ad6853 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:34:54 +0200 Subject: [PATCH 23/27] Fix test v4.24.0-rc1 --- test/extract_declaration.expected.out | 56 ++++++++++++++------------- 1 file changed, 29 insertions(+), 27 deletions(-) diff --git a/test/extract_declaration.expected.out b/test/extract_declaration.expected.out index 23458139..965f3d37 100644 --- a/test/extract_declaration.expected.out +++ b/test/extract_declaration.expected.out @@ -302,24 +302,24 @@ "pp": " := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", "constants": - ["ParserDescr.cat._@._hyg.202", - "ParserDescr.symbol._@._hyg.202", - "ParserDescr.binary._@._hyg.202", - "ParserDescr.trailingNode._@._hyg.202"]}, + ["ParserDescr.binary._@.3937598925._hygCtx._hyg.4", + "ParserDescr.trailingNode._@.3937598925._hygCtx._hyg.4", + "ParserDescr.symbol._@.3937598925._hygCtx._hyg.4", + "ParserDescr.cat._@.3937598925._hygCtx._hyg.4"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Lean.TrailingParserDescr ", - "constants": ["Lean.TrailingParserDescr._@._hyg.202"]}, + "constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Lean.TrailingParserDescr ", - "constants": ["Lean.TrailingParserDescr._@._hyg.202"]}, + "constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -332,10 +332,10 @@ "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": - " @[ scoped term_parser 1000 ] meta def «term_≋_» : Lean.TrailingParserDescr := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", + " @[ scoped term_parser 1000 ] public meta def «term_≋_» : Lean.TrailingParserDescr := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ", "name": "«term_≋_»", "modifiers": - {"visibility": "regular", + {"visibility": "public", "recKind": "default", "isUnsafe": false, "isProtected": false, @@ -353,25 +353,25 @@ "pp": " := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", "constants": - ["rhs._@._hyg.199", - "throw._@._hyg.221", - "Lean.Macro.Exception.unsupportedSyntax._@._hyg.221", + ["throw._@.3937598925._hygCtx._hyg.9", + "lhs._@.3937598925._hygCtx._hyg.3", "BEq.beq", - "lhs._@._hyg.199"]}, + "rhs._@.3937598925._hygCtx._hyg.3", + "Lean.Macro.Exception.unsupportedSyntax._@.3937598925._hygCtx._hyg.9"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Macro ", - "constants": ["Macro._@._hyg.221"]}, + "constants": ["Macro._@.3937598925._hygCtx._hyg.9"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Macro ", - "constants": ["Macro._@._hyg.221"]}, + "constants": ["Macro._@.3937598925._hygCtx._hyg.9"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -384,16 +384,16 @@ "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": - " @[ macro Demo.«term_≋_» ] meta def «_aux___macroRules_Demo_term_≋__1» : Macro := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", + " @[ scoped macro Demo.«term_≋_» ] public meta def «_aux___macroRules_Demo_term_≋__1» : Macro := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ", "name": "«_aux___macroRules_Demo_term_≋__1»", "modifiers": - {"visibility": "regular", + {"visibility": "public", "recKind": "default", "isUnsafe": false, "isProtected": false, "docString": null, "computeKind": "meta", - "attributes": ["macro Demo.«term_≋_»"]}, + "attributes": ["scoped macro Demo.«term_≋_»"]}, "kind": "definition", "fullName": "Demo.«_aux___macroRules_Demo_term_≋__1»", "binders": null}, @@ -405,26 +405,28 @@ "pp": " := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", "constants": - ["rhs._@._hyg.199", - "throw._@._hyg.201", - "_@._hyg.201", - "withRef._@._hyg.201", - "f._@._hyg.201", - "lhs._@._hyg.199"]}, + ["throw._@.3937598925._hygCtx._hyg.4", + "f._@.3937598925._hygCtx._hyg.4", + "lhs._@.3937598925._hygCtx._hyg.3", + "_@.3937598925._hygCtx._hyg.4", + "rhs._@.3937598925._hygCtx._hyg.3", + "withRef._@.3937598925._hygCtx._hyg.4"]}, "type": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " Lean.PrettyPrinter.Unexpander ", - "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]}, + "constants": + ["Lean.PrettyPrinter.Unexpander._@.3937598925._hygCtx._hyg.4"]}, "signature": {"range": {"synthetic": true, "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": " : Lean.PrettyPrinter.Unexpander ", - "constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]}, + "constants": + ["Lean.PrettyPrinter.Unexpander._@.3937598925._hygCtx._hyg.4"]}, "scope": {"varDecls": ["variable {α : Type u}"], "openDecl": [], @@ -437,10 +439,10 @@ "start": {"line": 35, "column": 0}, "finish": {"line": 35, "column": 32}}, "pp": - " @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", + " @[ scoped app_unexpander BEq.beq ] public meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ", "name": "_aux___unexpand_BEq_beq_1", "modifiers": - {"visibility": "regular", + {"visibility": "public", "recKind": "default", "isUnsafe": false, "isProtected": false, From 4ba900b5be284370984e72afdcb303047b65f164 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Wed, 19 Nov 2025 11:57:37 +0100 Subject: [PATCH 24/27] Fix ambiguous Syntax.Range --- REPL/JSON.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 3cfdaaaf..9ba761bc 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -122,7 +122,7 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : structure DocString where content : String - range : Syntax.Range + range : Elab.Syntax.Range deriving ToJson /-- See `Lean.Elab.Modifiers` -/ @@ -139,7 +139,7 @@ deriving ToJson structure DeclSignature where pp : String constants : Array Name - range : Syntax.Range + range : Elab.Syntax.Range deriving ToJson structure BinderView where @@ -159,19 +159,19 @@ structure DeclBinders where pp : String groups : Array String map : Array BinderView - range : Syntax.Range + range : Elab.Syntax.Range deriving ToJson structure DeclType where pp : String constants : Array Name - range : Syntax.Range + range : Elab.Syntax.Range deriving ToJson structure DeclValue where pp : String constants : Array Name - range : Syntax.Range + range : Elab.Syntax.Range deriving ToJson local instance : ToJson OpenDecl where @@ -194,7 +194,7 @@ deriving ToJson structure DeclarationInfo where pp: String - range : Syntax.Range + range : Elab.Syntax.Range scope : ScopeInfo name : Name fullName : Name From b5ff27e2781b9f92c35deea31ec7ae6da9c3eae7 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Sep 2025 18:43:08 +0200 Subject: [PATCH 25/27] Add `setOptions` to `CommandOptions` --- REPL/JSON.lean | 1 + REPL/Lean/InfoTree/ToJson.lean | 61 ++++++++++++++++++++++++++++++++++ REPL/Main.lean | 5 +-- 3 files changed, 65 insertions(+), 2 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 9ba761bc..5354f567 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -22,6 +22,7 @@ structure CommandOptions where -/ infotree : Option String incrementality : Option Bool := none -- whether to use incremental mode optimization + setOptions : Option Options := none /-- Run Lean commands. If `env = none`, starts a new session (in which you can use `import`). diff --git a/REPL/Lean/InfoTree/ToJson.lean b/REPL/Lean/InfoTree/ToJson.lean index 2598bb0b..562d607e 100644 --- a/REPL/Lean/InfoTree/ToJson.lean +++ b/REPL/Lean/InfoTree/ToJson.lean @@ -125,4 +125,65 @@ partial def InfoTree.toJson (t : InfoTree) (ctx? : Option ContextInfo) : IO Json return Lean.toJson (InfoTree.HoleJson.mk (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty) else throw <| IO.userError "No `ContextInfo` available." +instance : ToJson DataValue where + toJson (v : DataValue) : Json := + match v with + | .ofString s => toJson s + | .ofBool b => toJson b + | .ofName n => toJson n + | .ofNat n => toJson n + | .ofInt i => toJson i + | .ofSyntax _ => "" -- TODO: syntax to json + +instance KVMapToJson : ToJson KVMap where + toJson (m : KVMap) : Json := + Json.mkObj <| m.entries.map fun (k, v) => (k.toString, toJson v) + +instance : ToJson Options where + toJson (opts : Options) : Json := KVMapToJson.toJson opts + +def arrStrToName (arr : Array String) : Name := + if arr.isEmpty then Name.anonymous + else + arr.foldl (init := Name.anonymous) fun acc s => + if s.isEmpty then acc + else acc.append (Name.mkSimple s) + +instance : FromJson DataValue where + fromJson? (j : Json) : Except String DataValue := + match j with + | .str s => Except.ok <| DataValue.ofString s + | .bool b => Except.ok <| DataValue.ofBool b + | .num _ => match j.getNat? with + | Except.ok n => Except.ok <| DataValue.ofNat n + | Except.error _ => match j.getInt? with + | Except.ok i => Except.ok <| DataValue.ofInt i + | Except.error _ => Except.error "Invalid number format" + | .arr a => -- we parse array of strings as a Name + if a.all fun e => e.getStr? |>.isOk then + Except.ok <| DataValue.ofName (arrStrToName (a.map fun e => e.getStr?.toOption.getD "")) + else + Except.error "Unsupported JSON type for DataValue" + | _ => Except.error "Unsupported JSON type for DataValue" + +instance KVMapFromJson : FromJson KVMap where + fromJson? (j : Json) : Except String KVMap := + match j with + | .arr a => do -- array of (Name × DataValue) pairs to be converted to KVMap + let entries: Array (Name × DataValue) ← a.mapM fun e => do + match e with + | .arr #[.arr k, v] => do + let kName ← (if k.all fun e => e.getStr? |>.isOk then + Except.ok <| (arrStrToName (k.map fun e => e.getStr?.toOption.getD "")) + else + Except.error "Expected array of strings for Name") + let vData ← fromJson? v + return (kName, vData) + | _ => Except.error "Expected array of pairs for KVMap" + Except.ok <| KVMap.mk entries.toList + | _ => Except.error "Expected JSON object for KVMap" + +instance : FromJson Options where + fromJson? (j : Json) : Except String Options := KVMapFromJson.fromJson? j + end Lean.Elab diff --git a/REPL/Main.lean b/REPL/Main.lean index ff4422f4..b6201749 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -371,15 +371,16 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState let (initialCmdState, incStates, messages) ← try + let opts := s.setOptions.getD {} if s.incrementality.getD false then let bestIncrementalState? ← findBestIncrementalState s.cmd s.env - let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache + let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache opts -- Store the command text and incremental states for future reuse modify fun st => { st with headerCache := headerCache } recordCommandIncrementals s.cmd incStates s.env pure (initialCmdState, incStates, messages) else - let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {} + let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {} opts pure (initialCmdState, incStates, messages) catch ex => return .inr ⟨ex.toString⟩ From de6aff3b3d0f115ee5e4a54ec382e7168e37c4e5 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 22 Sep 2025 16:27:00 +0200 Subject: [PATCH 26/27] Fix elab async issue in tactic mode + add 2 new tests --- REPL/Snapshots.lean | 5 ++- test/app_type_mismatch2_parallel.expected.out | 41 +++++++++++++++++++ test/app_type_mismatch2_parallel.in | 14 +++++++ test/set_option.expected.out | 21 ++++++++++ test/set_option.in | 6 +++ 5 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 test/app_type_mismatch2_parallel.expected.out create mode 100644 test/app_type_mismatch2_parallel.in create mode 100644 test/set_option.expected.out create mode 100644 test/set_option.in diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index d87981e6..76a561f6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -211,9 +211,12 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option let s := match prevEnv? with | none => s | some env => { s with env } + let coreCtx ← readThe Core.Context + -- Ensure tactic snapshots run synchronously. + let coreCtx := { coreCtx with options := coreCtx.options.insert `Elab.async false } pure <| { coreState := s - coreContext := ← readThe Core.Context + coreContext := coreCtx metaState := ← getThe Meta.State metaContext := ← readThe Meta.Context termState := {} diff --git a/test/app_type_mismatch2_parallel.expected.out b/test/app_type_mismatch2_parallel.expected.out new file mode 100644 index 00000000..37d6afe7 --- /dev/null +++ b/test/app_type_mismatch2_parallel.expected.out @@ -0,0 +1,41 @@ +{"messages": + [{"severity": "error", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 7}, + "data": + "(kernel) application type mismatch\n @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n (have this := of_decide_eq_true (id (Eq.refl true));\n of_decide_eq_true (id (Eq.refl true)))\nargument has type\n true = true\nbut function has type\n (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b"}], + "env": 0} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 19}, + "goal": "⊢ 1 = 0", + "endPos": {"line": 1, "column": 24}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["case zero\n⊢ 0 = 0", "case succ\nn✝ : Nat\n⊢ n✝ + 1 = 0"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["case succ\nn✝ : Nat\n⊢ n✝ + 1 = 0"]} + +{"proofStatus": + "Error: kernel type check failed: (kernel) application type mismatch\n @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n (have this := of_decide_eq_true (id (Eq.refl true));\n of_decide_eq_true (id (Eq.refl true)))\nargument has type\n true = true\nbut function has type\n (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b", + "proofState": 3, + "goals": []} + +{"sorries": [{"proofState": 4, "goal": "n✝ : Nat\n⊢ true = true"}], + "proofStatus": "Incomplete: open goals remain", + "proofState": 5, + "goals": ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]} + +{"message": + "Lean error:\nTactic `apply` failed: could not unify the type of `?succ`\n n✝ + 1 = 0\nwith the goal\n true = true\n\nn✝ : Nat\n⊢ true = true"} + diff --git a/test/app_type_mismatch2_parallel.in b/test/app_type_mismatch2_parallel.in new file mode 100644 index 00000000..9714ecc4 --- /dev/null +++ b/test/app_type_mismatch2_parallel.in @@ -0,0 +1,14 @@ +{"cmd": "example : 1 = 0 := by\n cases 1\n rfl\n have: true := by\n apply ?succ\n trivial", "setOptions":[[["Elab","async"],true]]} + +{"cmd": "example : 1 = 0 := sorry", "setOptions":[[["Elab","async"],true]]} + +{"tactic": "cases 1", "proofState": 0} + +{"tactic": "rfl", "proofState": 1} + +{"tactic": "have: true := by\n apply ?succ\n trivial", "proofState": 2} + +{"tactic": "have: true := sorry", "proofState": 2} + +{"tactic": "apply ?succ", "proofState": 4} + diff --git a/test/set_option.expected.out b/test/set_option.expected.out new file mode 100644 index 00000000..5b30b955 --- /dev/null +++ b/test/set_option.expected.out @@ -0,0 +1,21 @@ +{"messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 8}, + "data": "Elab.async = false"}], + "env": 0} + +{"messages": + [{"severity": "info", + "pos": {"line": 10, "column": 0}, + "endPos": {"line": 10, "column": 8}, + "data": "Elab.async = true"}], + "env": 1} + +{"messages": + [{"severity": "info", + "pos": {"line": 8, "column": 0}, + "endPos": {"line": 8, "column": 8}, + "data": "Elab.async = true"}], + "env": 2} + diff --git a/test/set_option.in b/test/set_option.in new file mode 100644 index 00000000..ca54c591 --- /dev/null +++ b/test/set_option.in @@ -0,0 +1,6 @@ +{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"} + +{"cmd": "import Lean\nopen Lean Elab Command\n\nset_option Elab.async true\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"} + +{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp", "setOptions":[[["Elab","async"],true]]} + From a8f7b0a2b85aa33cc082501c4fa2b4a6cd8525ea Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 26 Sep 2025 12:19:06 +0200 Subject: [PATCH 27/27] Simplify test --- test/set_option.expected.out | 18 +++++++++--------- test/set_option.in | 6 +++--- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/test/set_option.expected.out b/test/set_option.expected.out index 5b30b955..3eec1407 100644 --- a/test/set_option.expected.out +++ b/test/set_option.expected.out @@ -1,21 +1,21 @@ {"messages": [{"severity": "info", - "pos": {"line": 8, "column": 0}, - "endPos": {"line": 8, "column": 8}, - "data": "Elab.async = false"}], + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 6}, + "data": "1 : Nat"}], "env": 0} {"messages": [{"severity": "info", - "pos": {"line": 10, "column": 0}, - "endPos": {"line": 10, "column": 8}, - "data": "Elab.async = true"}], + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 6}, + "data": "(1 : Nat) : Nat"}], "env": 1} {"messages": [{"severity": "info", - "pos": {"line": 8, "column": 0}, - "endPos": {"line": 8, "column": 8}, - "data": "Elab.async = true"}], + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 6}, + "data": "(1 : Nat) : Nat"}], "env": 2} diff --git a/test/set_option.in b/test/set_option.in index ca54c591..80fc2cb2 100644 --- a/test/set_option.in +++ b/test/set_option.in @@ -1,6 +1,6 @@ -{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"} +{"cmd": "#check 1"} -{"cmd": "import Lean\nopen Lean Elab Command\n\nset_option Elab.async true\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"} +{"cmd": "set_option pp.numericTypes true\n#check 1"} -{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n let o ← getOptions\n logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp", "setOptions":[[["Elab","async"],true]]} +{"cmd": "#check 1", "setOptions":[[["pp","numericTypes"],true]]}