Skip to content

MetricsSink #930

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.

Sign up for GitHub

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

Jump to bottom
Draft
dellaert wants to merge 10 commits into
base: master
Choose a base branch
from
Draft

MetricsSink #930

dellaert wants to merge 10 commits into from

Conversation

@dellaert
Copy link
Member

@dellaert dellaert commented Oct 20, 2025

  • Introduce a metrics sink interface (MetricsSink) so stages just call sink.record(...) and move on. The file sink writes JSON + regenerates the HTML on the output worker, keeping the Dask graph tidy. In addition, we can
  • turn off reporting altogether with +metrics_enabled=false
  • later add sqlite or postgres sinks

@dellaert dellaert removed the request for review from akshay-krishnan October 20, 2025 05:01
@dellaert dellaert marked this pull request as draft October 20, 2025 05:02
@dellaert
Copy link
Member Author

dellaert commented Oct 20, 2025

Putting as WIP as I noticed a number of issues that I will resolve first.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@liuzongyue6 liuzongyue6 Awaiting requested review from liuzongyue6

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@dellaert