Allows selecting a prover by its version number.

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

MIT License

321 stars 49 forks source link

Closed strub closed 12 months ago

strub commented 12 months ago

Syntax is name@version. The selected prover is the prover with name name and with the lowest version that is greater (or equal) than version.

For example, if Z3 4.8.0, Z3 4.8.2 & Z3 4.12.2 are installed, Z3@4.8 selects Z3 4.8.0.

strub commented 12 months ago

This is normal that the Jasmin eclib check fails. This failure can be fixed on the Jasmin side once this PR is merged.

strub commented 12 months ago

Looks good. PR description should be clarified: I'd expect 4.8 to select 4.8.0 if available, not 4.8.2.

Fixed. That's an error. 4.8 will select 4.8.0.

strub commented 12 months ago

Note that I plan to extend this with

allow exact match (4.8 will select the most recent version in the 4.8.x branch°
only if prover exists, s.t. you can tell which version of the prover you want, but you won't have any error if the prover is not installed at all.