Skip to content
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

server: record summarized error contents in telemetry #150

Merged
merged 3 commits into from
Jan 30, 2025

Conversation

samcowger
Copy link
Contributor

At present, telemetry events simply encode whether the event ended in success, failure, or neither. This expands the failure outcome to represent optional, additional context about the failure, and fills it with summaries of verification failures from Cerberus and CN.

This additional context is not particularly structured - it's basically the Cerberus/CN-defined pretty-printed version of the error, as a user would see in a tooltip. For example, here's how an error summary might appear in JSON-encoded telemetry:

{
  ...
  "causes": [
    "/Users/sam/projects/verse/cn-tutorial/src/examples/dll/add_orig.broken.c:15:9-27: Left-over unused resource 'Owned<struct dllist*>(&call_malloc__dllist0.return->next)(NULL)'"
  ],
  ...
}

I don't know whether this is a sufficient substitute for properly-structured error representations. In the longer term, I imagine that telemetry consumers would benefit from more structure, but I think there's definite value in the shorter term in providing at least something other than an opaque success/failure outcome.

@samcowger samcowger merged commit f567a5b into main Jan 30, 2025
2 checks passed
@samcowger samcowger deleted the sc/telemetry-errors branch January 30, 2025 16:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant