When reporting regressions (e.g., rocq-prover/rocq#20938 if it weren't already minimized), it would be nice to be able to tag the bot and ask it to minimize against two versions of Coq (a la CI minimization). Probably the way to do this is to have multiple opam switches with different versions of Coq installed. The buggy script could be run twice from different starting directories, once on the succeeding switch and then again on the failing switch. Success vs failure could be robustly automatically inferred by parsing the logs for both succeeding and erroring coqc calls, and looking for files on which both Rocq's were called, one succeed, and the other errored.
The invocation would be something like @coqbot regression minimize 8.18 9.0 followed by the script or file to be minimized.
When reporting regressions (e.g., rocq-prover/rocq#20938 if it weren't already minimized), it would be nice to be able to tag the bot and ask it to minimize against two versions of Coq (a la CI minimization). Probably the way to do this is to have multiple opam switches with different versions of Coq installed. The buggy script could be run twice from different starting directories, once on the succeeding switch and then again on the failing switch. Success vs failure could be robustly automatically inferred by parsing the logs for both succeeding and erroring coqc calls, and looking for files on which both Rocq's were called, one succeed, and the other errored.
The invocation would be something like
@coqbot regression minimize 8.18 9.0followed by the script or file to be minimized.