Lean.Server.Test.Runner

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

source

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

Type

freshPtr : USize
knownPtrs : Std.TreeMap USize USize compare

Instances For

source

@[reducible, inline]

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

Type

Instances For

source

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

Instances For

source

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

NormalizeM Lsp.RpcRef

Instances For

source

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

Type

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

Instances For

source

def Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo.fromJson :

Json → Except String SubexprInfo

Instances For

source

@[implicit_reducible]

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

FromJson SubexprInfo

source

def Lean.Server.Test.Runner.Client.instToJsonSubexprInfo.toJson :

SubexprInfo → Json

Instances For

source

@[implicit_reducible]

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

ToJson SubexprInfo

source

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

NormalizeM SubexprInfo

Instances For

source

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

Instances For

source

@[implicit_reducible]

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

FromJson Hyp

source

def Lean.Server.Test.Runner.Client.instFromJsonHyp.fromJson :

Json → Except String Hyp

Instances For

source

def Lean.Server.Test.Runner.Client.instToJsonHyp.toJson :

Hyp → Json

Instances For

source

@[implicit_reducible]

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

ToJson Hyp

source

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

NormalizeM Hyp

Instances For

source

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

Type

Instances For

source

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore.fromJson :

Json → Except String InteractiveGoalCore

Instances For

source

@[implicit_reducible]

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

FromJson InteractiveGoalCore

source

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore.toJson :

InteractiveGoalCore → Json

Instances For

source

@[implicit_reducible]

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

ToJson InteractiveGoalCore

source

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

NormalizeM InteractiveGoalCore

Instances For

source

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

Instances For

source

@[implicit_reducible]

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

FromJson InteractiveGoal

source

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal.fromJson :

Json → Except String InteractiveGoal

Instances For

source

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal.toJson :

InteractiveGoal → Json

Instances For

source

@[implicit_reducible]

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

ToJson InteractiveGoal

source

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

NormalizeM InteractiveGoal

Instances For

source

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

Type

goals : Array InteractiveGoal

Instances For

source

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals.fromJson :

Json → Except String InteractiveGoals

Instances For

source

@[implicit_reducible]

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

FromJson InteractiveGoals

source

@[implicit_reducible]

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

ToJson InteractiveGoals

source

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals.toJson :

InteractiveGoals → Json

Instances For

source

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

NormalizeM InteractiveGoals

Instances For

source

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

Type

Instances For

source

@[implicit_reducible]

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

FromJson InteractiveTermGoal

source

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal.fromJson :

Json → Except String InteractiveTermGoal

Instances For

source

@[implicit_reducible]

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

ToJson InteractiveTermGoal

source

def Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal.toJson :

InteractiveTermGoal → Json

Instances For

source

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

NormalizeM InteractiveTermGoal

Instances For

source

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

Type

id : Name
javascriptHash : UInt64
props : Json

Instances For

source

@[implicit_reducible]

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

FromJson WidgetInstance

source

def Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance.fromJson :

Json → Except String WidgetInstance

Instances For

source

@[implicit_reducible]

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

ToJson WidgetInstance

source

def Lean.Server.Test.Runner.Client.instToJsonWidgetInstance.toJson :

WidgetInstance → Json

Instances For

source

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

Type

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

Instances For

source

@[implicit_reducible]

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

FromJson (StrictOrLazy α✝ β✝)

source

def Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy.fromJson {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] :

Json → Except String (StrictOrLazy α✝ β✝)

Instances For

source

@[implicit_reducible]

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

ToJson (StrictOrLazy α✝ β✝)

source

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

StrictOrLazy α✝ β✝ → Json

Instances For

source

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

Instances For

source

@[implicit_reducible]

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

FromJson MsgEmbed

source

partial def Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed.fromJson :

Json → Except String MsgEmbed

source

partial def Lean.Server.Test.Runner.Client.instToJsonMsgEmbed.toJson :

MsgEmbed → Json

source

@[implicit_reducible]

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

ToJson MsgEmbed

source

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

NormalizeM MsgEmbed

source

@[reducible, inline]

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

Type

Instances For

source

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

InteractiveDiagnostic

Instances For

source

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

Array InteractiveDiagnostic

Instances For

source

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

Type

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

Instances For

source

@[implicit_reducible]

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

FromJson InfoPopup

source

def Lean.Server.Test.Runner.Client.instFromJsonInfoPopup.fromJson :

Json → Except String InfoPopup

Instances For

source

@[implicit_reducible]

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

ToJson InfoPopup

source

def Lean.Server.Test.Runner.Client.instToJsonInfoPopup.toJson :

InfoPopup → Json

Instances For

source

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

InfoPopup

Instances For

source

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

Type

kind : GoToKind
info : Lsp.RpcRef

Instances For

source

@[implicit_reducible]

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

FromJson GetGoToLocationParams

source

def Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams.fromJson :

Json → Except String GetGoToLocationParams

Instances For

source

def Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams.toJson :

GetGoToLocationParams → Json

Instances For

source

@[implicit_reducible]

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

ToJson GetGoToLocationParams

source

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

Type

query : String
msg : Widget.TaggedText MsgEmbed

Instances For

source

@[implicit_reducible]

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

FromJson HighlightMatchesParams

source

def Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams.fromJson :

Json → Except String HighlightMatchesParams

Instances For

source

@[implicit_reducible]

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

ToJson HighlightMatchesParams

source

def Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams.toJson :

HighlightMatchesParams → Json

Instances For

source

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

Type

subexpr (info : SubexprInfo) : HighlightedSubexprInfo
highlighted : HighlightedSubexprInfo

Instances For

source

@[implicit_reducible]

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

FromJson HighlightedSubexprInfo

source

def Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo.fromJson :

Json → Except String HighlightedSubexprInfo

Instances For

source

def Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo.toJson :

HighlightedSubexprInfo → Json

Instances For

source

@[implicit_reducible]

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

ToJson HighlightedSubexprInfo

source

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

HighlightedSubexprInfo → NormalizeM HighlightedSubexprInfo

Instances For

source

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

Instances For

source

partial def Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed.fromJson :

Json → Except String HighlightedMsgEmbed

source

@[implicit_reducible]

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

FromJson HighlightedMsgEmbed

source

@[implicit_reducible]

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

ToJson HighlightedMsgEmbed

source

partial def Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed.toJson :

HighlightedMsgEmbed → Json

source

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

NormalizeM HighlightedMsgEmbed

Test-only instances

source

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonPanelWidgetInstance :

FromJson Widget.PanelWidgetInstance

source

def Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse.fromJson :

Json → Except String Widget.GetWidgetsResponse

Instances For

source

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse :

FromJson Widget.GetWidgetsResponse

source

def Lean.Server.Test.Runner.word :

Std.Internal.Parsec.String.Parser String

Instances For

source

def Lean.Server.Test.Runner.ident :

Std.Internal.Parsec.String.Parser Name

Instances For

source

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

IO String

Instances For

source

partial def Lean.Server.Test.Runner.patchUris :

Json → IO Json

source

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

IO Unit

Instances For

source

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

Instances For

source

@[reducible, inline]

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

Type

Instances For

source

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

Lsp.Ipc.IpcM Unit

Instances For

source

def Lean.Server.Test.Runner.advanceRequestNo :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.advanceVersionNo :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.setSynced :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.setDesynced :

RunnerM Unit

Instances For

source

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

RunnerM β

Instances For

source

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

RunnerM β

Instances For

source

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

RunnerM Unit

Instances For

source

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

RunnerM β

Instances For

source

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

RunnerM β

Instances For

source

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

Instances For

source

def Lean.Server.Test.Runner.reset :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.skipLineWithDirective :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.skipLineWithoutDirective :

RunnerM Unit

Instances For

source

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

RunnerM Client.MsgEmbed

source

def Lean.Server.Test.Runner.processEdit :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processCollectDiagnostics :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processWaitForILeans :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processSync :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processWaitFor :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processCodeAction :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processInteractiveDiagnostics :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processGoals :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processTermGoal :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processWidgets :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processCompletion :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processIncomingCallHierarchy :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processOutgoingCallHierarchy :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processReferences :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processSymbols :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processModuleHierarchyImports :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processModuleHierarchyImportedBy :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processInlayHints :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processGenericRequest :

RunnerM Unit

Instances For

source

def Lean.Server.Test.Runner.processDirective (ws directive : String) (directiveTargetLineNo : Nat) :

RunnerM Unit

Instances For

source

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

RunnerM Unit

Instances For

source

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

IO Unit

Instances For