-
Notifications
You must be signed in to change notification settings - Fork 679
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 minimize
followed by an uploaded .v file (drag and drop or attached) @coqbot ci minimize
-
@coqbot ci minimize
followed by a list ofci-*
targets -
@coqbot resume ci minimize
followed by aci-
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 theminimize
, including things likecoq:8.16
orcoq.8.16
orcoq=8.16
orcoq-8.16
orocaml=4.08
, etc - Both
@coqbot minimize <options>
and@coqbot <options> ci minimize
and@coqbot <options> resume ci minimize
accept options likeinline-stdlib=yes
andextra-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 “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.