Add a --progress progress-bar option#1731
Conversation
|
No correctness or security regressions stood out in the PR diff ( Residual test gaps I’d still address:
I couldn’t run |
c0180a7 to
ea9c5a8
Compare
which only works in conjunction with --batch, not STDIN, as it needs to read over the file to count the number of goal statements. Care is also taken that a plain file, not a FIFO, is passed to --batch. Incidentally convert a neighboring string to triple quotes since it contained both single and double quotes.
ea9c5a8 to
bde0c16
Compare
Description
Add a
--progressprogress-bar option which only works in conjunction with--batch, not STDIN, as it needs to read over the file to count the number of goal statements.Care is also taken that a plain file, not a FIFO, is passed to
--batch.Incidentally convert a neighboring string to triple quotes since it contained both single and double quotes.
Motivation: the bar might be pretty, but the real value-add for big jobs is the ETA on the right.
Followups: the new code should really go into a
batch.py, but that is awaiting a refactor of the CLI arguments.Example:
Checklist
changelog.mdfile.AUTHORSfile (or it's already there).