-
Notifications
You must be signed in to change notification settings - Fork 708
Coqbot minimize feature
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 minimizefollowed by an uploaded .v file (drag and drop or attached) @coqbot ci minimize-
@coqbot ci minimizefollowed by a list ofci-*targets -
@coqbot resume ci minimizefollowed by aci-target, followed by a file (between triple backticks, or as a url or[description](url)to either the.vfile or to the.zipartifact from a github action (more details here)) to resume minimization at this stage. -
@coqbot minimizecan take options after theminimize, including things likecoq:8.16orcoq.8.16orcoq=8.16orcoq-8.16orocaml=4.08, etc - Both
@coqbot minimize <options>and@coqbot <options> ci minimizeand@coqbot <options> resume ci minimizeaccept options likeinline-stdlib=yesandextra-arg=--inline-prelude. Arguments toextra-arg=are passed along, unchanged, tofind-bug.py, though most arguments are not relevant for auto-minimization.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.