Before posting a comment, if minimization did not time out, and we're doing CI minimization on the main Rocq repo, we could create PRs that automatically add test-cases to the test-suite:
A new file should be added to the test-suite indicating the PR number and the CI dev from which the test was minimized. If a file already exists (with different contents, after removing the comment header on the first couple of lines), we can add a numeric suffix.
Maybe we could add a bot-rocq-prover-fork repo to rocq-community to create PRs from.
The branch could include the hash of the test-suite file, and we could check that no branch already exists with the specified file.
Before posting a comment, if minimization did not time out, and we're doing CI minimization on the main Rocq repo, we could create PRs that automatically add test-cases to the test-suite:
A new file should be added to the test-suite indicating the PR number and the CI dev from which the test was minimized. If a file already exists (with different contents, after removing the comment header on the first couple of lines), we can add a numeric suffix.
Maybe we could add a bot-rocq-prover-fork repo to rocq-community to create PRs from.
The branch could include the hash of the test-suite file, and we could check that no branch already exists with the specified file.