coq-community / run-coq-bug-minimizer

Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
MIT License
2 stars 0 forks source link

Add survey to coqbot response #9

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

@Zimmi48 @achlipala Does the wording in early-feedback.md look good to you?

@Zimmi48 Could you make @coqbot stick the PR/Issue number in the file coqbot.issue-number?

achlipala commented 3 years ago

The message wording looks good to me.

Zimmi48 commented 3 years ago

Hum, how do we handle the case of minimization being auto-restarted after a timeout? We usually need to pass some info back to coqbot via a stamp. This would have to be adapted to contain the issue number as well.

Zimmi48 commented 3 years ago

I forgot that this is also my job to fill this stamp. Will do then.

Zimmi48 commented 3 years ago

See coq/bot#168. If you could review it, that would be great!