AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
22 stars 1 forks source link

Add Nix support and CI #4

Closed W95Psp closed 9 months ago

W95Psp commented 9 months ago

This PR:

This PR requires https://github.com/FStarLang/karamel/pull/405. Currently, the karamel branch nix-expose-lib is hardcoded: I will rebase once https://github.com/FStarLang/karamel/pull/405 is merged.

Note: the first build will be slow, and then things will get cached!

W95Psp commented 9 months ago

Nice, will do! :)

Yes that would indeed be great! However, I'm wondering whether this Kyber workflow should live on this repo or on libcrux' repo? Or both maybe. I guess the main point for Kyber is to catch Kyber changes that would make Eurydice produce bad code: for that matter that's better if the CI is yielded at every PR & push on Kyber, right? Another point is to make sure Eurydice is still working while bumping dependencies. So maybe at the end of latest.yaml I can include Kyber extraction and tests, wdyt?

Anyway, indeed this will be for a subsequent PR :)

msprotz commented 9 months ago

Both of your suggestions sound good! I'll happily take the subsequent PRs when you have time. Thanks so much