EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
320 stars 49 forks source link

New command prefix: `fail` #495

Closed strub closed 11 months ago

strub commented 11 months ago

This prefix indicates that the following command should fail and that the error has to be ignored. It is an actual error if the command does not fail.

In interactive mode, the error is printed (at [info] level).

The main purpose of fail is to allow to write more precise unit tests where one can indicate which command shoud actually fail.

strub commented 11 months ago

Looks good to me.

This is still open to the command failing in an unexpected way. Perhaps a (later) extension of this could optionally be parameterised by the expected error message. (For use in unit testing.)

One first thing to do would be to distinguish between parse errors, typing errors & other errors. Internally, we already have the distinction. Not sure whether we want to go to the level of error messages.