trace.profiler.output Firefox Profiler integration

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

structure Lean.Firefox.Milliseconds : Type

• ms : Float

def Lean.Firefox.instInhabitedMilliseconds.default : Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instInhabitedMilliseconds : Inhabited Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instCoeFloatMilliseconds : Coe Float Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instOfScientificMilliseconds : OfScientific Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instToJsonMilliseconds : ToJson Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instFromJsonMilliseconds : FromJson Milliseconds

@[implicit_reducible]

instance Lean.Firefox.instAddMilliseconds : Add Milliseconds

structure Lean.Firefox.Microseconds : Type

• μs : Float

@[implicit_reducible]

instance Lean.Firefox.instCoeFloatMicroseconds : Coe Float Microseconds

@[implicit_reducible]

instance Lean.Firefox.instOfScientificMicroseconds : OfScientific Microseconds

@[implicit_reducible]

instance Lean.Firefox.instToJsonMicroseconds : ToJson Microseconds

@[implicit_reducible]

instance Lean.Firefox.instFromJsonMicroseconds : FromJson Microseconds

structure Lean.Firefox.Category : Type

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

def Lean.Firefox.instFromJsonCategory.fromJson : Json → Except String Category

@[implicit_reducible]

instance Lean.Firefox.instFromJsonCategory : FromJson Category

@[implicit_reducible]

instance Lean.Firefox.instToJsonCategory : ToJson Category

def Lean.Firefox.instToJsonCategory.toJson : Category → Json

structure Lean.Firefox.SampleUnits : Type

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

def Lean.Firefox.instFromJsonSampleUnits.fromJson : Json → Except String SampleUnits

@[implicit_reducible]

instance Lean.Firefox.instFromJsonSampleUnits : FromJson SampleUnits

def Lean.Firefox.instToJsonSampleUnits.toJson : SampleUnits → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonSampleUnits : ToJson SampleUnits

structure Lean.Firefox.ProfileMeta : Type

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

@[implicit_reducible]

instance Lean.Firefox.instFromJsonProfileMeta : FromJson ProfileMeta

def Lean.Firefox.instFromJsonProfileMeta.fromJson : Json → Except String ProfileMeta

@[implicit_reducible]

instance Lean.Firefox.instToJsonProfileMeta : ToJson ProfileMeta

def Lean.Firefox.instToJsonProfileMeta.toJson : ProfileMeta → Json

structure Lean.Firefox.StackTable : Type

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

def Lean.Firefox.instFromJsonStackTable.fromJson : Json → Except String StackTable

@[implicit_reducible]

instance Lean.Firefox.instFromJsonStackTable : FromJson StackTable

@[implicit_reducible]

instance Lean.Firefox.instToJsonStackTable : ToJson StackTable

def Lean.Firefox.instToJsonStackTable.toJson : StackTable → Json

structure Lean.Firefox.SamplesTable : Type

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

@[implicit_reducible]

instance Lean.Firefox.instFromJsonSamplesTable : FromJson SamplesTable

def Lean.Firefox.instFromJsonSamplesTable.fromJson : Json → Except String SamplesTable

@[implicit_reducible]

instance Lean.Firefox.instToJsonSamplesTable : ToJson SamplesTable

def Lean.Firefox.instToJsonSamplesTable.toJson : SamplesTable → Json

structure Lean.Firefox.FuncTable : Type

• 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

@[implicit_reducible]

instance Lean.Firefox.instFromJsonFuncTable : FromJson FuncTable

def Lean.Firefox.instFromJsonFuncTable.fromJson : Json → Except String FuncTable

def Lean.Firefox.instToJsonFuncTable.toJson : FuncTable → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonFuncTable : ToJson FuncTable

structure Lean.Firefox.FrameTable.Entry : Type

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

• 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

def Lean.Firefox.instFromJsonFrameTable.fromJson : Json → Except String FrameTable

@[implicit_reducible]

instance Lean.Firefox.instFromJsonFrameTable : FromJson FrameTable

def Lean.Firefox.instToJsonFrameTable.toJson : FrameTable → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonFrameTable : ToJson FrameTable

def Lean.Firefox.instInhabitedFrameTable.default : FrameTable

@[implicit_reducible]

instance Lean.Firefox.instInhabitedFrameTable : Inhabited FrameTable

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

Push an entry into a frame table.

structure Lean.Firefox.RawMarkerTable : Type

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

def Lean.Firefox.instFromJsonRawMarkerTable.fromJson : Json → Except String RawMarkerTable

@[implicit_reducible]

instance Lean.Firefox.instFromJsonRawMarkerTable : FromJson RawMarkerTable

def Lean.Firefox.instToJsonRawMarkerTable.toJson : RawMarkerTable → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonRawMarkerTable : ToJson RawMarkerTable

structure Lean.Firefox.ResourceTable : Type

• type : Array Json
• length : Nat

def Lean.Firefox.instFromJsonResourceTable.fromJson : Json → Except String ResourceTable

@[implicit_reducible]

instance Lean.Firefox.instFromJsonResourceTable : FromJson ResourceTable

def Lean.Firefox.instToJsonResourceTable.toJson : ResourceTable → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonResourceTable : ToJson ResourceTable

structure Lean.Firefox.Thread : Type

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

def Lean.Firefox.instFromJsonThread.fromJson : Json → Except String Thread

@[implicit_reducible]

instance Lean.Firefox.instFromJsonThread : FromJson Thread

@[implicit_reducible]

instance Lean.Firefox.instToJsonThread : ToJson Thread

def Lean.Firefox.instToJsonThread.toJson : Thread → Json

structure Lean.Firefox.Profile : Type

• meta : ProfileMeta
• libs : Array Json
• threads : Array Thread

def Lean.Firefox.instFromJsonProfile.fromJson : Json → Except String Profile

@[implicit_reducible]

instance Lean.Firefox.instFromJsonProfile : FromJson Profile

def Lean.Firefox.instToJsonProfile.toJson : Profile → Json

@[implicit_reducible]

instance Lean.Firefox.instToJsonProfile : ToJson Profile

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

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
• nativeSymbols : 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 : Array Category

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

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

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

• name : String
• processType : String
• isMainThread : Bool
• samples : SamplesTable
• markers : RawMarkerTable
• stackTable : StackTable
• frameTable : FrameTable
• resourceTable : ResourceTable
• nativeSymbols : 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) : Option 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.