Documentation

Lean.Util.Profiler

trace.profiler.output Firefox Profiler integration

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

structure Lean.Firefox.Milliseconds :

ms : Float

Instances For

instance Lean.Firefox.instInhabitedMilliseconds :

Inhabited Milliseconds

Equations

Lean.Firefox.instInhabitedMilliseconds = { default := { ms := default } }

instance Lean.Firefox.instCoeFloatMilliseconds :

Coe Float Milliseconds

Equations

Lean.Firefox.instCoeFloatMilliseconds = { coe := fun (s : Float) => { ms := s * 1000 } }

instance Lean.Firefox.instOfScientificMilliseconds :

OfScientific Milliseconds

Equations

Lean.Firefox.instOfScientificMilliseconds = { ofScientific := fun (m : Nat) (s : Bool) (e : Nat) => { ms := OfScientific.ofScientific m s e } }

instance Lean.Firefox.instToJsonMilliseconds :

ToJson Milliseconds

Equations

Lean.Firefox.instToJsonMilliseconds = { toJson := fun (x : Lean.Firefox.Milliseconds) => Lean.toJson x.ms }

instance Lean.Firefox.instFromJsonMilliseconds :

FromJson Milliseconds

Equations

Lean.Firefox.instFromJsonMilliseconds = { fromJson? := fun (j : Lean.Json) => Lean.Firefox.Milliseconds.mk <$> Lean.fromJson? j }

instance Lean.Firefox.instAddMilliseconds :

Add Milliseconds

Equations

Lean.Firefox.instAddMilliseconds = { add := fun (x y : Lean.Firefox.Milliseconds) => { ms := x.ms + y.ms } }

structure Lean.Firefox.Microseconds :

μs : Float

Instances For

instance Lean.Firefox.instCoeFloatMicroseconds :

Coe Float Microseconds

Equations

Lean.Firefox.instCoeFloatMicroseconds = { coe := fun (s : Float) => { μs := s * 1000000 } }

instance Lean.Firefox.instOfScientificMicroseconds :

OfScientific Microseconds

Equations

Lean.Firefox.instOfScientificMicroseconds = { ofScientific := fun (m : Nat) (s : Bool) (e : Nat) => { μs := OfScientific.ofScientific m s e } }

instance Lean.Firefox.instToJsonMicroseconds :

ToJson Microseconds

Equations

Lean.Firefox.instToJsonMicroseconds = { toJson := fun (x : Lean.Firefox.Microseconds) => Lean.toJson x.μs }

instance Lean.Firefox.instFromJsonMicroseconds :

FromJson Microseconds

Equations

Lean.Firefox.instFromJsonMicroseconds = { fromJson? := fun (j : Lean.Json) => Lean.Firefox.Microseconds.mk <$> Lean.fromJson? j }

structure Lean.Firefox.Category :

name : Name
color : String
subcategories : Array String

Instances For

instance Lean.Firefox.instFromJsonCategory :

FromJson Category

Equations

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

instance Lean.Firefox.instToJsonCategory :

ToJson Category

Equations

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

structure Lean.Firefox.SampleUnits :

time : String
eventDelay : String
threadCPUDelta : String

Instances For

instance Lean.Firefox.instFromJsonSampleUnits :

FromJson SampleUnits

Equations

Lean.Firefox.instFromJsonSampleUnits = { fromJson? := Lean.Firefox.fromJsonSampleUnits✝ }

instance Lean.Firefox.instToJsonSampleUnits :

ToJson SampleUnits

Equations

Lean.Firefox.instToJsonSampleUnits = { toJson := Lean.Firefox.toJsonSampleUnits✝ }

structure Lean.Firefox.ProfileMeta :

interval : Milliseconds
startTime : Milliseconds
categories : Array Category
processType : Nat
product : String
preprocessedProfileVersion : Nat
markerSchema : Array Json
sampleUnits : SampleUnits

Instances For

instance Lean.Firefox.instFromJsonProfileMeta :

FromJson ProfileMeta

Equations

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

instance Lean.Firefox.instToJsonProfileMeta :

ToJson ProfileMeta

Equations

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

structure Lean.Firefox.StackTable :

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

Instances For

instance Lean.Firefox.instFromJsonStackTable :

FromJson StackTable

Equations

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

instance Lean.Firefox.instToJsonStackTable :

ToJson StackTable

Equations

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

structure Lean.Firefox.SamplesTable :

stack : Array Nat
time : Array Milliseconds
weight : Array Milliseconds
weightType : String
threadCPUDelta : Array Microseconds
length : Nat

Instances For

instance Lean.Firefox.instFromJsonSamplesTable :

FromJson SamplesTable

Equations

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

instance Lean.Firefox.instToJsonSamplesTable :

ToJson SamplesTable

Equations

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

structure Lean.Firefox.FuncTable :

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

Instances For

instance Lean.Firefox.instFromJsonFuncTable :

FromJson FuncTable

Equations

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

instance Lean.Firefox.instToJsonFuncTable :

ToJson FuncTable

Equations

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

structure Lean.Firefox.FrameTable.Entry :

address : Int
inlineDepth : Nat
category : Option Nat
subcategory : Option Nat
func : Nat
nativeSymbol : Option Json
innerWindowID : Option Json
implementation : Option Json
line : Option Nat
column : Option Nat

structure Lean.Firefox.FrameTable :

address : Array Int
inlineDepth : Array Nat
category : Array (Option Nat)
subcategory : Array (Option Nat)
func : Array Nat
nativeSymbol : Array (Option Json)
innerWindowID : Array (Option Json)
implementation : Array (Option Json)
line : Array (Option Nat)
column : Array (Option Nat)
length : Nat

Instances For

instance Lean.Firefox.instFromJsonFrameTable :

FromJson FrameTable

Equations

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

instance Lean.Firefox.instToJsonFrameTable :

ToJson FrameTable

Equations

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

instance Lean.Firefox.instInhabitedFrameTable :

Inhabited FrameTable

Equations

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

def Lean.Firefox.FrameTable.push (t : FrameTable) (e : Entry) :

Push an entry into a frame table.

Equations

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

structure Lean.Firefox.RawMarkerTable :

data : Array Json
name : Array Json
length : Nat

Instances For

instance Lean.Firefox.instFromJsonRawMarkerTable :

FromJson RawMarkerTable

Equations

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

instance Lean.Firefox.instToJsonRawMarkerTable :

ToJson RawMarkerTable

Equations

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

structure Lean.Firefox.ResourceTable :

type : Array Json
length : Nat

Instances For

instance Lean.Firefox.instFromJsonResourceTable :

FromJson ResourceTable

Equations

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

instance Lean.Firefox.instToJsonResourceTable :

ToJson ResourceTable

Equations

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

structure Lean.Firefox.Thread :

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

Instances For

instance Lean.Firefox.instFromJsonThread :

FromJson Thread

Equations

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

instance Lean.Firefox.instToJsonThread :

Equations

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

structure Lean.Firefox.Profile :

meta : ProfileMeta
libs : Array Json
threads : Array Thread

Instances For

instance Lean.Firefox.instFromJsonProfile :

FromJson Profile

Equations

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

instance Lean.Firefox.instToJsonProfile :

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 : SamplesTable
markers : RawMarkerTable
stackTable : StackTable
frameTable : FrameTable
resourceTable : ResourceTable
stringArray : Array String
funcTable : 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 :

Equations

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

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

Equations

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

def Lean.Firefox.Profile.export (name : String) (startTime : Float) (traceStates : Array TraceState) (opts : Options) :

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 : SamplesTable
markers : RawMarkerTable
stackTable : StackTable
frameTable : FrameTable
resourceTable : ResourceTable
stringArray : Array String
funcTable : 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 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.