Stream: Coq devs & plugin devs

Topic: Automatic re-test of bugs

view this post on Zulip Emilio Jesús Gallego Arias (Aug 13 2021 at 13:02):

Hi folks, the work @Ali Caglayan has been doing on checking if old bug reports are valid made me think if we could automate it somehow, the idea would be to mark the reproduction case in the comment of the issue, so a script check_issue 8342 could be run and print "still an issue" or "seems solved in commit xxx".

Actually that could be made to work directly by requiring that all issues add an entry on the test suite when submitted

view this post on Zulip Ali Caglayan (Aug 13 2021 at 13:04):


view this post on Zulip Ali Caglayan (Aug 13 2021 at 13:19):

There are also the related suggestions of @Théo Zimmermann and @Jason Gross to get the bug minimizer to automatically tackle issues and produce a minimal example. We could perhaps get coqbot to automatically submit a PR adding these examples to the open bugs area of the test-suite.

Then when people submit patches, coqbot could automatically check the test-suite to see if there are any bugs that are closed, and we could get the patch author to execute a script that moves the bugs to the closed section (or output if needed).

This way, bugs are closed when the PR happens rather than months later.

view this post on Zulip Théo Zimmermann (Aug 13 2021 at 17:05):

My suggestion in coq#14621 was even more similar to Emilio's. The idea was to have a template with a well-specified space for a reproducible example so that coqbot could verify that they are still current periodically (and update the description to include all the tested versions). And I was thinking that this would supersede the open section of the test-suite which I would then suggest removing. (I don't think it's very valuable to have tests to check that some random bug hasn't been accidentally closed that are run every time we want to verify we haven't broken anything. And it doesn't scale.)

Last updated: Oct 16 2021 at 09:07 UTC