Stream: Coq devs & plugin devs

Topic: test-suite


view this post on Zulip Jason Gross (Apr 04 2021 at 15:58):

@Emilio Jesús Gallego Arias I see that you are closing a bunch of stale bugs. Should we add tests to the test-suite for all of the bugs that have test-cases which now succeed?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:11):

That would be great indeed, I thought about doing that myself for a few, but I sadly ran out of time for this :/ Should be easy to collect the bugs that need a test case and file a quick issue to gather them.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:12):

Maybe we could have a tag with: reproducible case

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:12):

that would mean "this issue has a test case that can be tested in the test-suite`

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:12):

or needs: test-suite update

view this post on Zulip Théo Zimmermann (Apr 04 2021 at 18:04):

Yes, with such a label, we could have coqbot periodically check that they are still open (instead of adding them to bugs/open).


Last updated: Apr 20 2024 at 01:41 UTC