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
21 stars 1 forks source link

Simplify synchronization with Charon #23

Closed Nadrieril closed 3 months ago

Nadrieril commented 3 months ago

I propose to copy the workflow we use in Aeneas to synchronize changes between Charon and Eurydice. The proposed workflow is as follows: when a PR is made to Charon that requires changes to Eurydice, we prepare the corresponding change to Eurydice, run make update-charon-pin, and submit a PR.

This will point the flake.lock at the right Charon branch, so the CI checks on the Eurydice side will be green. The exception is the new check-charon-pin CI check, which stays red until the Charon PR is merged. This is to avoid accidents where e.g. we rebase a branch and the flake.lock points to a commit that doesn't exist anymore. It also ensures we don't pick a charon commit that is older than before.

Once the Aeneas and Eurydice PRs are ready and green (with the exception of the check-charon-pin check), we can merge everything in any order.

msprotz commented 3 months ago

Neat. Thanks.