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

coqbot should track uses of the minimizer itself #184

Open
JasonGross opened this issue Dec 14, 2021 · 3 comments
Open

coqbot should track uses of the minimizer itself #184

JasonGross opened this issue Dec 14, 2021 · 3 comments
Labels
bug minimizer enhancement New feature or request

Comments

@JasonGross
Copy link
Member

Probably by commenting on coq-community/run-coq-bug-minimizer#8, or editing a comment there, with some log of uses.

Possible data that's useful to track:

  • PRs that minimization was possible on
  • PRs that minimization was triggered on
  • Duration, time, trigerrer, and stats about minimization for each minimization run, and any emoji reactions to that run
@JasonGross
Copy link
Member Author

Thoughts:
We could include in the "I've started minimization" comment a unique identifier and other debug information (including #130, how the minimization was triggered, by whom, etc), all hidden by code folding. Then when posting the final comment, the minimizer could use this unique identifier to fetch the relevant debug info, and also post a comment to coq-community/run-coq-bug-minimizer#8 with the relevant info (we should be careful not to tag anyone on that thread, though) (new comment rather than edit comment to avoid github comment length limits and to avoid race conditions).

@JasonGross
Copy link
Member Author

Alternatively, we could just make text files in, e.g., a logging branch of run-coq-bug-minimizer (perhaps making a folder for each PR and for each UID and for each ci target) (name of text file could be current-time---random-sequence.txt)

@JasonGross
Copy link
Member Author

Possibly use GraphQL API for adding files

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug minimizer enhancement New feature or request
Projects
Status: Todo
Development

No branches or pull requests

1 participant