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

Remove F* in flake #88

Open msprotz opened 1 day ago

msprotz commented 1 day ago

Until https://github.com/FStarLang/karamel/issues/496 is fixed

msprotz commented 20 hours ago

@Nadrieril how can I instruct Nix to run only "make minimal" in karamel, so that the build does not require an F* dependency?

Nadrieril commented 20 hours ago

I don't really understand the setup, but I'd change the flake in karamel to have an option for that. That means either a new karamel-minimal output or a callPackage option. I can attempt a PR tomorrow if you want

msprotz commented 20 hours ago

Yeah if that's ok it would be great -- you can probably do it much faster than I can. Basically if you invoke only "make minimal" in krml it builds without F*.

Nadrieril commented 4 hours ago

Karamel itself uses FSTAR_HOME="dummy" in their flake (here), could we just do that too?