Jason Gross
Jason Gross
See https://github.com/coq/coq/pull/15860#issuecomment-1080460118 for motivation. I want to be able to write @coqbot bench coq-fiat-crypto-with-bedrock. Ideally coqbot would let me know immediately if any of the packages don't exist in the...
https://github.com/coq/coq/pull/15807#issuecomment-1077917098 : You requested minimization of suggested failing CI jobs, but no jobs were suggested at commit fb47d4f. You can trigger minimization of ci-analysis with ci minimize all or by...
The issue is that ci-analysis also fails on master. Coqbot should report the reason it suggests not minimizing targets when we request that it minimize them anyway, at least when...
@Zimmi48 do you know what's up with the following failures? - ci-sf failed because https://gitlab.com/coq/coq/-/jobs/1991212828/artifacts/download is a 404, idk what's up here - ci-itauto failed because https://gitlab.com/coq/coq/-/jobs/1991212857/artifacts/download is a 404...
Example: https://github.com/coq-community/run-coq-bug-minimizer/issues/2#issuecomment-1031448739 Currently we only resume on ci minimization jobs.
It may make sense to have coqbot compose the reply comment instead (this would also allow coqbot to do the truncation of the file only for the comment and not...
https://github.com/coq/coq/pull/14748#issuecomment-1003116849
"could not be found among the jobs lint" is mis-pluralized in https://github.com/coq/coq/pull/14748#issuecomment-1003116849, and maybe we should indicate what the list of jobs we're reporting is (is "lint" a candidate for...
There's a hidden target `` and a misleading target `ci-unimath` at https://github.com/coq/coq/pull/14748#issuecomment-1003116849
Currently there's no indication that a target was doubled in the request, even though it only triggers once. https://github.com/coq/coq/pull/14748#issuecomment-1003120077