-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Extend the workaround in the v53 upgrader to generate missing subcategory columns. #5369
base: main
Are you sure you want to change the base?
Conversation
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #5369 +/- ##
=======================================
Coverage 85.96% 85.96%
=======================================
Files 312 312
Lines 30331 30330 -1
Branches 8295 8296 +1
=======================================
+ Hits 26073 26074 +1
+ Misses 3661 3659 -2
Partials 597 597 ☔ View full report in Codecov by Sentry. |
5ae2cd7
to
217755f
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the quick patch!
I see some inconsistencies with the older version on some vernier profiles. Please see my comment below.
// frameTable.subcategory, such as the ones generated by Lean before | ||
// https://github.com/leanprover/lean4/pull/6363 or the ones generated by | ||
// vernier before https://github.com/jhawthorn/vernier/issues/128 . | ||
if (!frameTable.category || !frameTable.subcategory) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What happens if the profile has category
but doesn't have subcategory
? Currently that's the case for vernier. And we are actually removing the category data of vernier and rewriting it with the categories that are in the stack table. Which could potentially be wrong.
I think this is okay for most of the case, but when I compared the example profiles, I find some inconsistencies.
For example, this is how this profile looks like before #5342:
And this is how it looks like after this PR:
So it looks like some of the samples are attributed as "idle" now, and it wasn't the case before.
Looking at the samples, and I see that Kernel#system
frame was the "other" category and now it's "idle". I'm not familiar with Ruby, but it chatgpt says that in Ruby, Kernel#system
is a method that executes a command in a subshell. So I don't think idle is correct here.
What do you think?
I think for vernier profiles, I would prefer to keep the frameTable.category
information if they have it, instead of removing it completely.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for double-checking that! After making that change, the activity graph still looks different though - now there's no idle category at all any more! So I think this profile uses the same frame for stacks with different categories, some of them idle and some of them non-idle. This cannot be expressed in the new format - you'd need distinct frames with different frame categories. That's very interesting!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've changed the code to keep the category column and just generate a zero subcategory column. With zero instead of null, I was hoping that the call node tooltip in the flame graph would no longer show ": undefined" but it still does. I haven't looked into why.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've also added comments to express all the constraints that the front-end has for the category information. I'm not sure why I didn't write those comments when I first added those fields. Oh well.
217755f
to
16fd7ef
Compare
Production | Deploy preview
Fixes #5368.