search

EasyCrypt / easycrypt

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

[nix] vendor prover derivations #436

Closed fdupress closed 1 year ago

fdupress commented 1 year ago

This vendors derivations for provers known to work with our pinned why3, independently of updates to nixpkgs—allowing us to move ahead if we decide to stick to an LTS or to stay behind if we keep in line with unstable.

This should improve reproducibility of external checks we run, and of checks run externally.

fdupress commented 1 year ago

CVC5 spits out loads of HiFailures on the standard lib and examples. I am not entirely sure I trust its stability and reproducibility right now.

We could, however, try to be helpful and contribute failure samples.

strub commented 1 year ago

I misread your diff. There is a pin for CVC4 and CVC5.

However, we should investigate the CVC5 failures. Unless I am wrong, CVC4 is not maintained anymore.

fdupress commented 1 year ago

Before I merge... I just realised that I didn't credit nixpkgs when I lifted their derivations to adapt. I'm planning on putting a local copy of the MIT license into the scripts/nix/ folder with the appropriate copyright notice. Anything else you'd like me to do to acknowledge this?

strub commented 1 year ago

Fine by me.