Runner for tests/lean/interactive server tests. Put here to avoid repeated elaboration overhead per test.

structure Lean.Server.Test.Runner.Client.NormalizeState : Type

• freshPtr : USize
• knownPtrs : Std.TreeMap USize USize compare

@[reducible, inline]

abbrev Lean.Server.Test.Runner.Client.NormalizeM (α : Type) : Type

def Lean.Server.Test.Runner.Client.NormalizeM.run {α : Type} (x : NormalizeM α) (s : NormalizeState) : α

def Lean.Server.Test.Runner.Client.normalizedRef (ref : Lsp.RpcRef) : NormalizeM Lsp.RpcRef

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonRpcRef : ToJson Lsp.RpcRef

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonRpcRef : FromJson Lsp.RpcRef

structure Lean.Server.Test.Runner.Client.SubexprInfo : Type

• info : Lsp.RpcRef
• subexprPos : String
• diffStatus? : Option String

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo : FromJson SubexprInfo

def Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo.fromJson : Json → Except String SubexprInfo

def Lean.Server.Test.Runner.Client.instToJsonSubexprInfo.toJson : SubexprInfo → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonSubexprInfo : ToJson SubexprInfo

def Lean.Server.Test.Runner.Client.SubexprInfo.normalize (i : SubexprInfo) : NormalizeM SubexprInfo

structure Lean.Server.Test.Runner.Client.Hyp : Type

• type : Widget.TaggedText SubexprInfo
• names : Array String
• fvarIds : Array FVarId
• val? : Option (Widget.TaggedText SubexprInfo)
• isInstance? : Option Bool
• isType? : Option Bool
• isInserted? : Option Bool
• isRemoved? : Option Bool

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHyp : FromJson Hyp

def Lean.Server.Test.Runner.Client.instFromJsonHyp.fromJson : Json → Except String Hyp

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHyp : ToJson Hyp

def Lean.Server.Test.Runner.Client.instToJsonHyp.toJson : Hyp → Json

def Lean.Server.Test.Runner.Client.Hyp.normalize (h : Hyp) : NormalizeM Hyp

structure Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore : FromJson InteractiveGoalCore

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore.fromJson : Json → Except String InteractiveGoalCore

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore : ToJson InteractiveGoalCore

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore.toJson : InteractiveGoalCore → Json

def Lean.Server.Test.Runner.Client.InteractiveGoalCore.normalize (g : InteractiveGoalCore) : NormalizeM InteractiveGoalCore

structure Lean.Server.Test.Runner.Client.InteractiveGoalextends Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef
• userName? : Option String
• goalPrefix : String
• mvarId : MVarId
• isInserted? : Option Bool
• isRemoved? : Option Bool

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal : FromJson InteractiveGoal

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal.fromJson : Json → Except String InteractiveGoal

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal.toJson : InteractiveGoal → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal : ToJson InteractiveGoal

def Lean.Server.Test.Runner.Client.InteractiveGoal.normalize (goal : InteractiveGoal) : NormalizeM InteractiveGoal

structure Lean.Server.Test.Runner.Client.InteractiveGoals : Type

• goals : Array InteractiveGoal

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals : FromJson InteractiveGoals

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals.fromJson : Json → Except String InteractiveGoals

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals : ToJson InteractiveGoals

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals.toJson : InteractiveGoals → Json

def Lean.Server.Test.Runner.Client.InteractiveGoals.normalize (gs : InteractiveGoals) : NormalizeM InteractiveGoals

structure Lean.Server.Test.Runner.Client.InteractiveTermGoalextends Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef
• range : Lsp.Range
• term : Lsp.RpcRef

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal.fromJson : Json → Except String InteractiveTermGoal

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal : FromJson InteractiveTermGoal

def Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal.toJson : InteractiveTermGoal → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal : ToJson InteractiveTermGoal

def Lean.Server.Test.Runner.Client.InteractiveTermGoal.normalize (g : InteractiveTermGoal) : NormalizeM InteractiveTermGoal

structure Lean.Server.Test.Runner.Client.WidgetInstance : Type

• id : Name
• javascriptHash : UInt64
• props : Json

def Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance.fromJson : Json → Except String WidgetInstance

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance : FromJson WidgetInstance

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonWidgetInstance : ToJson WidgetInstance

def Lean.Server.Test.Runner.Client.instToJsonWidgetInstance.toJson : WidgetInstance → Json

inductive Lean.Server.Test.Runner.Client.StrictOrLazy (α β : Type) : Type

• strict {α β : Type} : α → StrictOrLazy α β
• lazy {α β : Type} : β → StrictOrLazy α β

def Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy.fromJson {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] : Json → Except String (StrictOrLazy α✝ β✝)

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] : FromJson (StrictOrLazy α✝ β✝)

def Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy.toJson {α✝ β✝ : Type} [ToJson α✝] [ToJson β✝] : StrictOrLazy α✝ β✝ → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy {α✝ β✝ : Type} [ToJson α✝] [ToJson β✝] : ToJson (StrictOrLazy α✝ β✝)

inductive Lean.Server.Test.Runner.Client.MsgEmbed : Type

• expr : Widget.TaggedText SubexprInfo → MsgEmbed
• goal : InteractiveGoal → MsgEmbed
• widget (wi : WidgetInstance) (alt : Widget.TaggedText MsgEmbed) : MsgEmbed
• trace (indent : Nat) (cls : Name) (msg : Widget.TaggedText MsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (Widget.TaggedText MsgEmbed)) Lsp.RpcRef) : MsgEmbed

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed : FromJson MsgEmbed

partial def Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed.fromJson : Json → Except String MsgEmbed

partial def Lean.Server.Test.Runner.Client.instToJsonMsgEmbed.toJson : MsgEmbed → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonMsgEmbed : ToJson MsgEmbed

partial def Lean.Server.Test.Runner.Client.MsgEmbed.normalize (m : MsgEmbed) : NormalizeM MsgEmbed

@[reducible, inline]

abbrev Lean.Server.Test.Runner.Client.InteractiveDiagnostic : Type

def Lean.Server.Test.Runner.Client.InteractiveDiagnostic.normalize (d : InteractiveDiagnostic) : InteractiveDiagnostic

def Lean.Server.Test.Runner.Client.normalizeInteractiveDiagnostics (diags : Array InteractiveDiagnostic) : Array InteractiveDiagnostic

structure Lean.Server.Test.Runner.Client.InfoPopup : Type

• type : Option (Widget.TaggedText SubexprInfo)
• exprExplicit : Option (Widget.TaggedText SubexprInfo)
• doc : Option String

def Lean.Server.Test.Runner.Client.instFromJsonInfoPopup.fromJson : Json → Except String InfoPopup

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInfoPopup : FromJson InfoPopup

def Lean.Server.Test.Runner.Client.instToJsonInfoPopup.toJson : InfoPopup → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInfoPopup : ToJson InfoPopup

def Lean.Server.Test.Runner.Client.InfoPopup.normalize (p : InfoPopup) : InfoPopup

structure Lean.Server.Test.Runner.Client.GetGoToLocationParams : Type

• kind : GoToKind
• info : Lsp.RpcRef

def Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams.fromJson : Json → Except String GetGoToLocationParams

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams : FromJson GetGoToLocationParams

def Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams.toJson : GetGoToLocationParams → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams : ToJson GetGoToLocationParams

structure Lean.Server.Test.Runner.Client.HighlightMatchesParams : Type

• query : String
• msg : Widget.TaggedText MsgEmbed

def Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams.fromJson : Json → Except String HighlightMatchesParams

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams : FromJson HighlightMatchesParams

def Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams.toJson : HighlightMatchesParams → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams : ToJson HighlightMatchesParams

inductive Lean.Server.Test.Runner.Client.HighlightedSubexprInfo : Type

• subexpr (info : SubexprInfo) : HighlightedSubexprInfo
• highlighted : HighlightedSubexprInfo

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo : FromJson HighlightedSubexprInfo

def Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo.fromJson : Json → Except String HighlightedSubexprInfo

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo : ToJson HighlightedSubexprInfo

def Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo.toJson : HighlightedSubexprInfo → Json

def Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.normalize : HighlightedSubexprInfo → NormalizeM HighlightedSubexprInfo

inductive Lean.Server.Test.Runner.Client.HighlightedMsgEmbed : Type

• expr : Widget.TaggedText HighlightedSubexprInfo → HighlightedMsgEmbed
• goal : InteractiveGoal → HighlightedMsgEmbed
• widget (wi : WidgetInstance) (alt : Widget.TaggedText HighlightedMsgEmbed) : HighlightedMsgEmbed
• trace (indent : Nat) (cls : Name) (msg : Widget.TaggedText HighlightedMsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (Widget.TaggedText HighlightedMsgEmbed)) Lsp.RpcRef) : HighlightedMsgEmbed
• highlighted : HighlightedMsgEmbed

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed : FromJson HighlightedMsgEmbed

partial def Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed.fromJson : Json → Except String HighlightedMsgEmbed

partial def Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed.toJson : HighlightedMsgEmbed → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed : ToJson HighlightedMsgEmbed

partial def Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.normalize (m : HighlightedMsgEmbed) : NormalizeM HighlightedMsgEmbed

Test-only instances

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonPanelWidgetInstance : FromJson Widget.PanelWidgetInstance

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse : FromJson Widget.GetWidgetsResponse

def Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse.fromJson : Json → Except String Widget.GetWidgetsResponse

def Lean.Widget.GetWidgetsResponse.debugJson (r : GetWidgetsResponse) : Json

def Lean.Server.Test.Runner.word : Std.Internal.Parsec.String.Parser String

def Lean.Server.Test.Runner.ident : Std.Internal.Parsec.String.Parser Name

def Lean.Server.Test.Runner.patchUri (s : String) : IO String

partial def Lean.Server.Test.Runner.patchUris : Json → IO Json

def Lean.Server.Test.Runner.printOutputLn (j : Json) : IO Unit

structure Lean.Server.Test.Runner.RunnerState : Type

• uri : Lsp.DocumentUri
• synced : Bool
• rpcSessionId : Option UInt64
• lineNo : Nat
• lastActualLineNo : Nat
• pos : Lsp.Position
• method : String
• params : String
• versionNo : Nat
• requestNo : Nat

@[reducible, inline]

abbrev Lean.Server.Test.Runner.RunnerM (α : Type) : Type

def Lean.Server.Test.Runner.RunnerM.run {α : Type} (act : RunnerM α) (init : RunnerState) : Lsp.Ipc.IpcM Unit

def Lean.Server.Test.Runner.advanceRequestNo : RunnerM Unit

def Lean.Server.Test.Runner.advanceVersionNo : RunnerM Unit

def Lean.Server.Test.Runner.setSynced : RunnerM Unit

def Lean.Server.Test.Runner.setDesynced : RunnerM Unit

def Lean.Server.Test.Runner.request {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type) [FromJson β] : RunnerM β

def Lean.Server.Test.Runner.requestWithLoggedResponse {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type) [FromJson β] [ToJson β] (logParam : Bool := true) : RunnerM β

def Lean.Server.Test.Runner.logResponse {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type := Json) [FromJson β] [ToJson β] (logParam : Bool := true) : RunnerM Unit

def Lean.Server.Test.Runner.rpcRequest {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type) [FromJson β] : RunnerM β

def Lean.Server.Test.Runner.rpcRequestWithLoggedResponse {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type) [FromJson β] [ToJson β] (logParam : Bool := true) (normalize : β → Client.NormalizeM β := pure) : RunnerM β

def Lean.Server.Test.Runner.logRpcResponse {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type := Json) [FromJson β] [ToJson β] (logParam : Bool := true) (normalize : β → Client.NormalizeM β := pure) : RunnerM Unit

def Lean.Server.Test.Runner.reset : RunnerM Unit

def Lean.Server.Test.Runner.skipLineWithDirective : RunnerM Unit

def Lean.Server.Test.Runner.skipLineWithoutDirective : RunnerM Unit

partial def Lean.Server.Test.Runner.expandTraces (msg : Client.MsgEmbed) : RunnerM Client.MsgEmbed

def Lean.Server.Test.Runner.processEdit : RunnerM Unit

def Lean.Server.Test.Runner.processCollectDiagnostics : RunnerM Unit

def Lean.Server.Test.Runner.processWaitForILeans : RunnerM Unit

def Lean.Server.Test.Runner.processSync : RunnerM Unit

def Lean.Server.Test.Runner.waitForMessage (msg : String) : Lsp.Ipc.IpcM Unit

Waits for a textDocument/publishDiagnostics notification with a specific message to be emitted. Discards all received messages, so should not be combined with Ipc.collectDiagnostics. Used to implement the waitFor test directive.

If the server reports a $/lean/fileProgress notification with fatalError kind, this aborts with an error rather than blocking forever: the message we are waiting for will never be produced (the worker either crashed or its header processing failed fatally, so no body elaboration will run).

Kept here rather than in Lean.Lsp.Ipc because it is specifically a test-driver helper rather than a general-purpose IPC primitive.

def Lean.Server.Test.Runner.processWaitFor : RunnerM Unit

def Lean.Server.Test.Runner.processCodeAction : RunnerM Unit

def Lean.Server.Test.Runner.processInteractiveDiagnostics : RunnerM Unit

def Lean.Server.Test.Runner.processGoals : RunnerM Unit

def Lean.Server.Test.Runner.processTermGoal : RunnerM Unit

def Lean.Server.Test.Runner.processWidgets : RunnerM Unit

def Lean.Server.Test.Runner.processCompletion : RunnerM Unit

def Lean.Server.Test.Runner.processIncomingCallHierarchy : RunnerM Unit

def Lean.Server.Test.Runner.processOutgoingCallHierarchy : RunnerM Unit

def Lean.Server.Test.Runner.processReferences : RunnerM Unit

def Lean.Server.Test.Runner.processSymbols : RunnerM Unit

def Lean.Server.Test.Runner.processModuleHierarchyImports : RunnerM Unit

def Lean.Server.Test.Runner.processModuleHierarchyImportedBy : RunnerM Unit

def Lean.Server.Test.Runner.processInlayHints : RunnerM Unit

def Lean.Server.Test.Runner.processGenericRequest : RunnerM Unit

def Lean.Server.Test.Runner.processDirective (_ws directive : String) (directiveTargetLineNo directiveTargetColumn : Nat) : RunnerM Unit

def Lean.Server.Test.Runner.processLine (line : String) : RunnerM Unit

def Lean.Server.Test.Runner.main (args : List String) : IO Unit