feat: serve trace.profiler data via local HTTP server#13530
Merged
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Kha
commented
May 6, 2026
Comment on lines
+69
to
+74
| /-- | ||
| The local socket address the server is bound to. When `serve` is called with a port of `0`, this | ||
| reflects the ephemeral port assigned by the OS rather than the requested address. | ||
| `none` for servers constructed without an associated listening socket (e.g. `serveConnection`). | ||
| -/ | ||
| localAddr : Option Net.SocketAddress := none |
Comment on lines
+67
to
+70
| let _ ← Async.ofAsyncTask (.ofPurePromise done) | ||
| -- The handler signals `doneCh` before the response body is written; brief pause so the writer | ||
| -- can drain before `shutdownAndWait` cancels its task. | ||
| Async.sleep 200 |
Member
There was a problem hiding this comment.
Right now it's not avoidable :S
Member
Author
There was a problem hiding this comment.
It seems like a quite special use case, not sure other APIs have a solution for that?
Member
There was a problem hiding this comment.
Yes, after looking more closely at the use case I agree.
This PR adds a `trace.profiler.serve` option that, when enabled, serves the Firefox Profiler-compatible profile JSON on an ephemeral `127.0.0.1` port and opens `https://profiler.firefox.com/from-url/...` in the user's default browser, à la `samply`. The server shuts down once the profile has been fetched. Compared to `trace.profiler.output`, which writes the profile to a file that the user must then manually upload to `profiler.firefox.com`, this is a single-command workflow. Implementation notes: * `Std.Http.Server` now exposes the bound socket address so the caller can read back the OS-assigned ephemeral port when binding to port `0`. * `addTraceAsMessages` and the import-time trace recording now check a shared `trace.profiler.isExporting` predicate; the previous `trace.profiler.output`-only check would otherwise consume the trace state before serving could see it. * `interpreter.prefer_native` is enabled in stage0 so the new `trace.profiler.serve` option getter can be invoked from compile-time elaboration in stage1.
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
trace.profiler.serveoption that, when enabled, serves the Firefox Profiler-compatible profile JSON on an ephemeral127.0.0.1port and openshttps://profiler.firefox.com/from-url/...in the user's default browser, à lasamply. The server shuts down once the profile has been fetched.Compared to
trace.profiler.output, which writes the profile to a file that the user must then manually upload toprofiler.firefox.com, this is a single-command workflow not touching the file system.Implementation notes:
Std.Http.Servernow exposes the bound socket address so the caller can read back the OS-assigned ephemeral port when binding to port0.addTraceAsMessagesand the import-time trace recording now check a sharedtrace.profiler.isExportingpredicate; the previoustrace.profiler.output-only check would otherwise consume the trace state before serving could see it.