From 816ceb5e83674501608f93bdea152f938ccd87aa Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 10 Dec 2024 14:46:56 -0800
Subject: [PATCH] fix: add missing category fields to Lean.Firefox.FrameTable

See https://github.com/firefox-devtools/profiler/issues/5254
---
 src/Lean/Util/Profiler.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Util/Profiler.lean b/src/Lean/Util/Profiler.lean
index 3da0c31678ae..86db7f1ae5f0 100644
--- a/src/Lean/Util/Profiler.lean
+++ b/src/Lean/Util/Profiler.lean
@@ -83,6 +83,8 @@ structure FuncTable where
 deriving FromJson, ToJson
 
 structure FrameTable where
+  category : Array Nat
+  subcategory : Array Nat
   func : Array Nat
   inlineDepth : Array Json := #[]
   innerWindowID : Array Json := #[]
@@ -182,6 +184,8 @@ where
             }
             frameTable := {
               func := thread.frameTable.func.push thread.funcMap.size
+              category := thread.frameTable.category.push category
+              subcategory := thread.frameTable.subcategory.push 0
               length := thread.frameTable.length + 1
             }
             funcMap := thread.funcMap.insert strIdx thread.funcMap.size })
@@ -230,7 +234,7 @@ def Thread.new (name : String) : Thread := {
   name
   samples := { stack := #[], time := #[], weight := #[], threadCPUDelta := #[], length := 0 }
   stackTable := { frame := #[], «prefix» := #[], category := #[], subcategory := #[], length := 0 }
-  frameTable := { func := #[], length := 0 }
+  frameTable := { func := #[], category := #[], subcategory := #[], length := 0 }
   stringArray := #[]
   funcTable := {
     name := #[], resource := #[], fileName := #[], lineNumber := #[], columnNumber := #[],