Skip to content

Commit

Permalink
Update discussion of bug minimizer
Browse files Browse the repository at this point in the history
Co-authored-by: Jason Gross <[email protected]>
  • Loading branch information
jdchristensen and JasonGross authored Sep 17, 2024
1 parent 2b11db0 commit 5a5221f
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions STYLE.md
Original file line number Diff line number Diff line change
Expand Up @@ -1441,10 +1441,10 @@ available in his [coq-tools][coq-tools] repository. To use it:
it as much as possible.

You will need to pass the bug-finder several arguments to tell it to
use the HoTT version of Coq and where to find the rest of the library;
pass the right flags and where to find the rest of the library;
a common invocation would be something like

$ /path/to/find-bug.py --coqc .../coqc --coqtop .../coqtop -R . HoTT Path/To/Buggy.v bug_minimized.v
$ /path/to/find-bug.py --arg -noinit --arg -indices-matter -R . HoTT Path/To/Buggy.v bug_minimized.v

When it exits, the minimized code producing the bug will be in
`bug_minimized.v`.
Expand Down

0 comments on commit 5a5221f

Please sign in to comment.