search

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

Rely on upstream fixes to disable systematic desugaring of array assi… #5

Closed msprotz closed 6 months ago

msprotz commented 6 months ago

…gnments, which in turn leads to much prettier code-gen.

msprotz commented 6 months ago

@W95Psp is this using the latest krml master? it looks like this build hasn't picked up my upstream fixes... thanks!!

W95Psp commented 6 months ago

hi @msprotz, indeed, dependencies are all pinned and locked! I pushed an update.

If you have Nix installed, you can nix flake update to update every dependencies, and then commit the flake.lock file. (or nix flake lock --update-input INPUT to update an input INPUT, with INPUT being a key of inputs in flake.nix)

msprotz commented 6 months ago

Thanks! That already allowed me to uncover another issue.

Is there a way to always pick the latest version available? Pinning a version of Charon has little value for me. For me, the main appeal of CI is being notified as soon as Charon changes something upstream so that I can catch up.

W95Psp commented 6 months ago

The nightly job is picking the latest version of everything actually! so if anything goes wrong with new Charon/Krml/F*/whatever, the nighlty job will fail

This PR/push job is testing against pinned dependencies, we can change that, but it is a bit weird with respect to the lockfile

msprotz commented 6 months ago

Ah ok perfect! I didn't realize that was the purpose of the nightly. Sounds great then. Cheers!