Skip to content

Make :check, :exhaust, :prove, etc more gracefully interruptible #98

@acfoltzer

Description

@acfoltzer

We can interrupt these commands with Ctrl-C, but we don't get nice output about how far it managed to make it, etc. Cryptol 1 had something more like this:

Cryptol> :exhaust \x -> (x:[100]) >= 0
Will exhaustively run 2^100 inputs. (Use Ctrl-C to stop.)
Checking case 5051 of 2^100 (3.98e-25%)%)
*** Interrupted, 1267650600228229401496703200325 untested. 5050 passed, 1 failed. (Total run: 5051.)
*** Success rate: 99.98%. (5050 of 5051)

We should at least report how many cases we've made it through for :check and :exhaust.

Metadata

Metadata

Assignees

Labels

feature requestAsking for new or improved functionality

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions