Add proof status bar

[nwatson22]

Adds a rich.progress.Progress bar to track proofs as they are running. This includes a timer which stops when the proof completes, the ID of the proof, a status which tracks the overall stage of proof execution: [Loading proof, Starting KoreServer, Initializing proof, Running proof, Finished], and a summary which is proof-type specific but which for APRProofs shows their status and number of total, pending, passed, failing, vacuous, and stuck nodes, and number of branches. If multiple proofs are proven in the same batch (the same _run_cfg_group call) in sequence, the bars for the thus far completed proofs remain grouped at the bottom of the screen with the currently running proof.

This only works in single-proof mode, i.e. where we run init_and_run_proof directly rather than through multiprocess. A different bar is displayed for the multiprocess mode, which shows the number of proofs finished, total number of proofs, how many passed and how many failed, and the number of workers requested. Unfortunately the display with the multiprocess mode is a bit buggy, though still usable. The worker processes aren't aware of updates to the progress bar, so when they emit a log message, they update the progress bar to its default state, so it appears to "flicker" back to its default state when --verbose is turned on in this mode. For this same reason I was unable to add the proofs as additional bars as they finish in this mode. This is not an issue with single-proof parallelism because there all the log printing is done on one process.

To facilitate the multiprocess mode, I changed from using map to apply_async to be able to run code upon completion of each task. I also bypass the multiprocessing in the case where multiple workers were requested but there is only one proof selected.

The status bar is enabled by default on kontrol prove. To disable it pass --hide-status-bar.

[anvacaru]

Overall it looks great! I added some screenshots below.

A couple suggestions:

• maybe also adding terminal nodes to the list?
• is it possible by any chance to replace / with \n and display the different nodes on multiple lines?

0:01:12 test%GLDTokenTest.testTransferFailure_0(address,uint256,bytes32):0 Finished PASSED
    6 nodes
    0 pending
    1 passed
    0 failing
    0 branches
    0 vacuous
    0 stuck

 - 

[nwatson22]

@anvacaru The terminal nodes count is easy to add, I will open another PR in pyk to do that. There are a couple reasons why I'm displaying it on one line. When you run multiple proofs (with --workers 1, so it doesn't try to run them on different processes), it will continue displaying the bar for each proof after it completed so you see a summary of all completed proofs:

Also, the progress bar library I'm using works in columns, so I don't know how I'd get the node summary to align like in your example. the PASSED/3 nodes/0 pending/1 passed/0 failing/0 branches/0 vacuous/2 terminal /0 stuck is all one unit, and if I split it up with newlines the whole thing will end up looking more like this:

which could be OK although it's somewhat jarring as the length of the columns change and the tall column shifts around.

[anvacaru]

@nwatson22 Thank you for looking into this! Then it makes sense to keep it on one line. I didn't execute multiple proofs 😅 . Perhaps it would improve the readability if you would replace the column separator with | ? The current one / might be confused with the division? I don't know.

[nwatson22]

@nwatson22 Thank you for looking into this! Then it makes sense to keep it on one line. I didn't execute multiple proofs 😅 . Perhaps it would improve the readability if you would replace the column separator with | ? The current one / might be confused with the division? I don't know.

@anvacaru I opened a branch in the k repo here which does both these: runtimeverification/k#4566