Coqbot minimize feature - rocq-prover/rocq GitHub Wiki

One can tell @coqbot to generate a shorter version of a single Coq file reproducing its original bug. To do so, you can write a comment of the form @coqbot: minimize immediately followed by a bash script compiling the buggy file with coqc. The script must be surrounded with triple quotes.

For example:

@coqbot: minimize
```bash
#!/usr/bin/env bash
opam install -y coq-ext-lib
eval $(opam env)
mkdir temp
cd temp
wget https://github.com/coq/coq/files/4698509/bug.v.zip
unzip bug.v.zip
coqc -q bug.v
```

The coqc invocation does not need to be done by the script itself, for instance it can be done through a make invocation.

You can also directly minimize a .v file, like

@coqbot minimize
```coq
Fail Check True.
```

Coqbot autominimization also supports the following features (to be documented more later):

• @coqbot minimize followed by an uploaded .v file (drag and drop or attached)
• @coqbot ci minimize
• @coqbot ci minimize followed by a list of ci-* targets
• @coqbot resume ci minimize followed by a ci- target, followed by a file (between triple backticks, or as a url or [description](url) to either the .v file or to the .zip artifact from a github action (more details here)) to resume minimization at this stage.
• @coqbot minimize can take options after the minimize, including things like coq:8.16 or coq.8.16 or coq=8.16 or coq-8.16 or ocaml=4.08, etc
• Both @coqbot minimize <options> and @coqbot <options> ci minimize and @coqbot <options> resume ci minimize accept options like inline-stdlib=yes and extra-arg=--inline-prelude. Arguments to extra-arg= are passed along, unchanged, to find-bug.py, though most arguments are not relevant for auto-minimization.