Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[nix] vendor prover derivations #436

Merged
merged 1 commit into from
Sep 13, 2023
Merged

[nix] vendor prover derivations #436

merged 1 commit into from
Sep 13, 2023

Conversation

fdupress
Copy link
Member

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 fdupress requested a review from strub September 12, 2023 16:00
@fdupress fdupress self-assigned this Sep 12, 2023
Copy link
Member

@strub strub left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we update the README file and the default set of provers to use CVC5 instead of CVC4?

@strub strub added this to the Release 2022.07 milestone Sep 12, 2023
@fdupress
Copy link
Member Author

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
Copy link
Member

strub commented Sep 13, 2023

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
Copy link
Member Author

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
Copy link
Member

strub commented Sep 13, 2023

Fine by me.

@fdupress fdupress merged commit 287106a into main Sep 13, 2023
12 checks passed
@fdupress fdupress deleted the nix-vendor-provers branch September 13, 2023 20:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants