Some scripts to help manipulate Coq developments
Some scripts to help construct small reproducing examples of bugs.
The script find-bug.py is the main program; run find-bug.py -h to
see the options. The script will ask you two questions: whether or
not it successfully determined the error you're seeking to reproduce,
and whether or not it created a regular expression which captures that
error. After that, it will run without user input until it finishes.
Standard usage is to invoke with the buggy file name and the output (minimized) file name:
python find-bug.py BUGGY_FILE.v OUTPUT_FILE.v
You can add -v for a more verbose output.
If you are using a non-system version of Coq, you can pass --coqtop /path/to/coqtop and --coqc /path/to/coqc. If you pass -R . Foo
to, say, coq_makefile, you can inform find-bug.py of this fact
using -R . Foo.
There is an example in the examples directory. You can run
run-example-01.sh to see how the program works. You can pass this
script the arguments -v, -vv, or -vvv for different levels of
verbosity. Look at the contents of run-example-01.sh to see how to
invoke the program.
Note that this program can fail in mysterious ways when run using Windows Python 2.7 under cygwin; it seems that buffering and stdin and stderr and Popen are screwed up. To work around this, there is a coqtop.bat file which is chosen as the default coqtop program. Somehow running via a .bat file makes things work. You will probably have to use a similar wrapper if you use a custom coqtop executable.
Additionally, quirks in module name resolution can result in inlining
failures (see #16), and
global side effects of Require can also result in failures (see
#41).
- Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. Automatic test-case reduction in proof assistants: A case study in Coq. ITP 2022
- Jason Gross. Coq Bug Minimizer, CoqPL 2015
The script minimize-requires.py can be used to remove unneeded Require
statements. Run minimize-requires.py -h to see the options.
Standard usage is to run
minimize-requires.py some-file1.v some-file2.v ... --in-place .bak
or, if you want to minimize an entire project,
minimize-requires.py --all -f _CoqProject
(you can add --in-place .bak if you want to save backup files)
The script proof-using-helper.py is the main program; run
proof-using-helper.py -h to see the options.
Standard usage is to invoke with the any -R arguments passed to Coq,
and either pipe the output of make quick with Global Set Suggest Proof Using
on, to this script, or to give it a file containing said output.
make quick -j -k | tee -a proof_using.log
python /path/to/proof-using-helper.py proof_using.log
You can add -v for a more verbose output.