Documentation

Lean.Util.Profiler

trace.profiler.output Firefox Profiler integration

Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.js

@[reducible, inline]

abbrev Lean.Firefox.Milliseconds :

Equations

Lean.Firefox.Milliseconds = Float

structure Lean.Firefox.Category :

name : String
color : String
subcategories : Array String

Instances For

instance Lean.Firefox.instFromJsonCategory :

Lean.FromJson Lean.Firefox.Category

Equations

Lean.Firefox.instFromJsonCategory = { fromJson? := Lean.Firefox.fromJsonCategory✝ }

instance Lean.Firefox.instToJsonCategory :

Lean.ToJson Lean.Firefox.Category

Equations

Lean.Firefox.instToJsonCategory = { toJson := Lean.Firefox.toJsonCategory✝ }

structure Lean.Firefox.ProfileMeta :

interval : Lean.Firefox.Milliseconds
startTime : Lean.Firefox.Milliseconds
categories : Array Lean.Firefox.Category
processType : Nat
product : String
preprocessedProfileVersion : Nat
markerSchema : Array Lean.Json

Instances For

instance Lean.Firefox.instFromJsonProfileMeta :

Lean.FromJson Lean.Firefox.ProfileMeta

Equations

Lean.Firefox.instFromJsonProfileMeta = { fromJson? := Lean.Firefox.fromJsonProfileMeta✝ }

instance Lean.Firefox.instToJsonProfileMeta :

Lean.ToJson Lean.Firefox.ProfileMeta

Equations

Lean.Firefox.instToJsonProfileMeta = { toJson := Lean.Firefox.toJsonProfileMeta✝ }

structure Lean.Firefox.StackTable :

frame : Array Nat
prefix : Array (Option Nat)
category : Array Nat
subcategory : Array Nat
length : Nat

Instances For

instance Lean.Firefox.instFromJsonStackTable :

Lean.FromJson Lean.Firefox.StackTable

Equations

Lean.Firefox.instFromJsonStackTable = { fromJson? := Lean.Firefox.fromJsonStackTable✝ }

instance Lean.Firefox.instToJsonStackTable :

Lean.ToJson Lean.Firefox.StackTable

Equations

Lean.Firefox.instToJsonStackTable = { toJson := Lean.Firefox.toJsonStackTable✝ }

structure Lean.Firefox.SamplesTable :

stack : Array Nat
time : Array Lean.Firefox.Milliseconds
weight : Array Lean.Firefox.Milliseconds
weightType : String
length : Nat

Instances For

instance Lean.Firefox.instFromJsonSamplesTable :

Lean.FromJson Lean.Firefox.SamplesTable

Equations

Lean.Firefox.instFromJsonSamplesTable = { fromJson? := Lean.Firefox.fromJsonSamplesTable✝ }

instance Lean.Firefox.instToJsonSamplesTable :

Lean.ToJson Lean.Firefox.SamplesTable

Equations

Lean.Firefox.instToJsonSamplesTable = { toJson := Lean.Firefox.toJsonSamplesTable✝ }

structure Lean.Firefox.FuncTable :

name : Array Nat
isJS : Array Lean.Json
relevantForJS : Array Lean.Json
resource : Array Int
fileName : Array (Option Nat)
lineNumber : Array (Option Nat)
columnNumber : Array (Option Nat)
length : Nat

Instances For

instance Lean.Firefox.instFromJsonFuncTable :

Lean.FromJson Lean.Firefox.FuncTable

Equations

Lean.Firefox.instFromJsonFuncTable = { fromJson? := Lean.Firefox.fromJsonFuncTable✝ }

instance Lean.Firefox.instToJsonFuncTable :

Lean.ToJson Lean.Firefox.FuncTable

Equations

Lean.Firefox.instToJsonFuncTable = { toJson := Lean.Firefox.toJsonFuncTable✝ }

structure Lean.Firefox.FrameTable :

func : Array Nat
inlineDepth : Array Lean.Json
innerWindowID : Array Lean.Json
length : Nat

Instances For

instance Lean.Firefox.instFromJsonFrameTable :

Lean.FromJson Lean.Firefox.FrameTable

Equations

Lean.Firefox.instFromJsonFrameTable = { fromJson? := Lean.Firefox.fromJsonFrameTable✝ }

instance Lean.Firefox.instToJsonFrameTable :

Lean.ToJson Lean.Firefox.FrameTable

Equations

Lean.Firefox.instToJsonFrameTable = { toJson := Lean.Firefox.toJsonFrameTable✝ }

structure Lean.Firefox.RawMarkerTable :

data : Array Lean.Json
name : Array Lean.Json
length : Nat

Instances For

instance Lean.Firefox.instFromJsonRawMarkerTable :

Lean.FromJson Lean.Firefox.RawMarkerTable

Equations

Lean.Firefox.instFromJsonRawMarkerTable = { fromJson? := Lean.Firefox.fromJsonRawMarkerTable✝ }

instance Lean.Firefox.instToJsonRawMarkerTable :

Lean.ToJson Lean.Firefox.RawMarkerTable

Equations

Lean.Firefox.instToJsonRawMarkerTable = { toJson := Lean.Firefox.toJsonRawMarkerTable✝ }

structure Lean.Firefox.ResourceTable :

type : Array Lean.Json
length : Nat

Instances For

instance Lean.Firefox.instFromJsonResourceTable :

Lean.FromJson Lean.Firefox.ResourceTable

Equations

Lean.Firefox.instFromJsonResourceTable = { fromJson? := Lean.Firefox.fromJsonResourceTable✝ }

instance Lean.Firefox.instToJsonResourceTable :

Lean.ToJson Lean.Firefox.ResourceTable

Equations

Lean.Firefox.instToJsonResourceTable = { toJson := Lean.Firefox.toJsonResourceTable✝ }

structure Lean.Firefox.Thread :

name : String
processType : String
isMainThread : Bool
samples : Lean.Firefox.SamplesTable
markers : Lean.Firefox.RawMarkerTable
stackTable : Lean.Firefox.StackTable
frameTable : Lean.Firefox.FrameTable
resourceTable : Lean.Firefox.ResourceTable
stringArray : Array String
funcTable : Lean.Firefox.FuncTable

Instances For

instance Lean.Firefox.instFromJsonThread :

Lean.FromJson Lean.Firefox.Thread

Equations

Lean.Firefox.instFromJsonThread = { fromJson? := Lean.Firefox.fromJsonThread✝ }

instance Lean.Firefox.instToJsonThread :

Lean.ToJson Lean.Firefox.Thread

Equations

Lean.Firefox.instToJsonThread = { toJson := Lean.Firefox.toJsonThread✝ }

structure Lean.Firefox.Profile :

Instances For

instance Lean.Firefox.instFromJsonProfile :

Lean.FromJson Lean.Firefox.Profile

Equations

Lean.Firefox.instFromJsonProfile = { fromJson? := Lean.Firefox.fromJsonProfile✝ }

instance Lean.Firefox.instToJsonProfile :

Lean.ToJson Lean.Firefox.Profile

Equations

Lean.Firefox.instToJsonProfile = { toJson := Lean.Firefox.toJsonProfile✝ }

structure Lean.Firefox.ThreadWithMapsextends Lean.Firefox.Thread :

Thread with maps necessary for computing max sharing indices

name : String
processType : String
isMainThread : Bool
samples : Lean.Firefox.SamplesTable
markers : Lean.Firefox.RawMarkerTable
stackTable : Lean.Firefox.StackTable
frameTable : Lean.Firefox.FrameTable
resourceTable : Lean.Firefox.ResourceTable
stringArray : Array String
funcTable : Lean.Firefox.FuncTable
stringMap : Std.HashMap String Nat
funcMap : Std.HashMap Nat Nat
stackMap : Std.HashMap (Nat × Option Nat) Nat
lastTime : Float
Last timestamp encountered: stop time of preceding sibling, or else start time of parent.

def Lean.Firefox.categories :

Array Lean.Firefox.Category

Equations

One or more equations did not get rendered due to their size.

def Lean.Firefox.Thread.new (name : String) :

Lean.Firefox.Thread

Equations

One or more equations did not get rendered due to their size.

def Lean.Firefox.Profile.export (name : String) (startTime : Lean.Firefox.Milliseconds) (traceState : Lean.TraceState) (opts : Lean.Options) :

IO Lean.Firefox.Profile

Equations

One or more equations did not get rendered due to their size.

structure Lean.Firefox.ThreadWithCollideMapsextends Lean.Firefox.ThreadWithMaps :

name : String
processType : String
isMainThread : Bool
samples : Lean.Firefox.SamplesTable
markers : Lean.Firefox.RawMarkerTable
stackTable : Lean.Firefox.StackTable
frameTable : Lean.Firefox.FrameTable
resourceTable : Lean.Firefox.ResourceTable
stringArray : Array String
funcTable : Lean.Firefox.FuncTable
stringMap : Std.HashMap String Nat
funcMap : Std.HashMap Nat Nat
stackMap : Std.HashMap (Nat × Option Nat) Nat
lastTime : Float
sampleMap : Std.HashMap Nat Nat
Max sharing map for samples

def Lean.Firefox.Profile.collide (ps : Array Lean.Firefox.Profile) :

Option Lean.Firefox.Profile

Merges given profiles such that samples with identical stacks are deduplicated by adding up their weights. Minimizes profile size while preserving per-stack timing information.

Equations

One or more equations did not get rendered due to their size.