nix: add a dev shell - Githubissues

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

nix: add a dev shell #21

Closed Nadrieril closed 3 months ago

Nadrieril commented 3 months ago

This PR does two things:

Adds a dev shell for nix users like me so we can easily develop on eurydice;
~Makes it so the nix builder (and thus the CI) reports warning as errors, because CI was missing errors like non-exhaustive matches. I set all warnings to be errors which might be a bit strong; we can tweak as needed.~

Nadrieril commented 3 months ago

With this Ci change we should likely coordinate breaking changes in charon with eurydice like we do for aeneas. The idea would be that if charon makes a breaking change, we wait for the appropriate PR to be ready on the eurydice side before merging both. Then for completeness we should also add kyber to eurydice's CI.

msprotz commented 3 months ago

This is great, thanks for looking into this. Two comments.

+A enables all warnings; @A turns all warnings as errors -- so your flag is inconsistent with your comment.
Enabling all warnings as errors is not recommended at all, since future versions of OCaml will most likely introduce new warnings. Although here it's just for nix...

Why not do like krml? https://github.com/FStarLang/karamel/blob/master/src/dune#L4

Nadrieril commented 3 months ago

I'm glad you know something about ocaml flags, I was just copying what we have for aeneas. I'll try some things tomorrow

Nadrieril commented 3 months ago

I removed the part about build flags, I'll figure that out later. I'd like the dev shell to be merged first because it makes my life easier

msprotz commented 3 months ago

Looking forward to the subsequent PR for warnings, and happy to chat about it with tomorrow morning if that helps (just ping me)

Nadrieril commented 2 months ago

It seems I failed to remove the part about build flags x) I might have gotten confused between this repo and my fork, oops. No harm caused though.

msprotz commented 2 months ago

Yeah I noticed it's fine. Can you submit a followup when you get a chance so that we can fix the build flag story?

Nadrieril commented 2 months ago

I wasn't particularly excited to dig into ocaml docs. Do you happen to know the right incantation? Afaik the only reason warnings are silenced is because we cuild in release mode, so maybe we only need to change the dune file?

msprotz commented 2 months ago

I vote for this in the various dune files:

(env
  (_
    (flags (:standard -warn-error -A -w @1-2@3-7@8..12@14..21@23..29-30@31..38-39-40-41@43@57))))

after https://github.com/FStarLang/karamel/blob/master/lib/dune#L27 -- the _ should ensure this is picked for both dev and release

msprotz commented 2 months ago

although -warn-error -A is probably redundant here -- I would only keep the -w part