trace.profiler.output Firefox Profiler integration

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

structure Lean.Firefox.Milliseconds : Type

• ms : Float

instance Lean.Firefox.instInhabitedMilliseconds : Inhabited Lean.Firefox.Milliseconds

Equations

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

instance Lean.Firefox.instCoeFloatMilliseconds : Coe Float Lean.Firefox.Milliseconds

Equations

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

instance Lean.Firefox.instOfScientificMilliseconds : OfScientific Lean.Firefox.Milliseconds

Equations

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

instance Lean.Firefox.instToJsonMilliseconds : Lean.ToJson Lean.Firefox.Milliseconds

Equations

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

instance Lean.Firefox.instFromJsonMilliseconds : Lean.FromJson Lean.Firefox.Milliseconds

Equations

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

instance Lean.Firefox.instAddMilliseconds : Add Lean.Firefox.Milliseconds

Equations

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

structure Lean.Firefox.Microseconds : Type

• μs : Float

instance Lean.Firefox.instCoeFloatMicroseconds : Coe Float Lean.Firefox.Microseconds

Equations

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

instance Lean.Firefox.instOfScientificMicroseconds : OfScientific Lean.Firefox.Microseconds

Equations

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

instance Lean.Firefox.instToJsonMicroseconds : Lean.ToJson Lean.Firefox.Microseconds

Equations

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

instance Lean.Firefox.instFromJsonMicroseconds : Lean.FromJson Lean.Firefox.Microseconds

Equations

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

structure Lean.Firefox.Category : Type

• name : String
• color : String
• subcategories : Array String

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.SampleUnits : Type

• time : String
• eventDelay : String
• threadCPUDelta : String

instance Lean.Firefox.instFromJsonSampleUnits : Lean.FromJson Lean.Firefox.SampleUnits

Equations

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

instance Lean.Firefox.instToJsonSampleUnits : Lean.ToJson Lean.Firefox.SampleUnits

Equations

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

structure Lean.Firefox.ProfileMeta : Type

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

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 : Type

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

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 : Type

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

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 : Type

• 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

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 : Type

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

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 : Type

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

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

• type : Array Lean.Json
• length : Nat

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 : Type

• 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

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 : Type

• meta : Lean.Firefox.ProfileMeta
• libs : Array Lean.Json
• threads : Array Lean.Firefox.Thread

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 : Type

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 : Float) (traceStates : Array 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 : Type

• 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.