Stream: coqbot devs & users

Topic: Encouraging test-suite inclusion of minimized test cases


view this post on Zulip Théo Zimmermann (Jun 03 2021 at 09:37):

One idea to encourage inclusion of minimized test cases in the test-suite: when the minimization succeeds and produces a file under a line limit TBD, add a command to ask coqbot to push a commit adding the test case to the test-suite (and advertise the command in the comment posted by coqbot).

view this post on Zulip Jason Gross (Jun 03 2021 at 15:40):

This would be cool! If we set the line limit to be something less than 32KiB (the point at which the minimizer truncates the minimized file), we could parse the test-suite file from the posted comment. Perhaps the command could be @coqbot add test-suite ci-XXXX, whence the bot looks for the most recent comment on the PR which starts with Minimized File [^ ]* .from ci-XXXX., and then takes the first block between triple-backticks to be added to the test-suite. It'll be pretty for me to include this suggestion from the minimizer side.

view this post on Zulip Théo Zimmermann (Jun 03 2021 at 18:17):

I would certainly put the limit below 32KiB (how many lines is that!?). You could also consider the comment to contain a unique identifier and the command to coqbot to use it.

view this post on Zulip Jason Gross (Jun 03 2021 at 23:10):

The 32KiB file at https://github.com/coq/coq/pull/14328#issuecomment-849175708 is 849 lines. The reason I truncate by bytes and not lines is that github comments have a 65536 byte limit. I allocate 32KiB (half the maximum) to the minimized file, and 1/8 the max to each of the intermediate file, the build log, and the minimization log. (This leaves 8KiB for miscellaneous text around the logs.) If you want a UID for each comment, that also sounds fine, and I can use the sha1sum or sha256sum of the minimized file as the UID.


Last updated: Jan 31 2023 at 11:01 UTC