check-world: add mls-star

[mtzguido]

cc @TWal, this adds mls-star to the check-world workflow. It starts from scratch in Nix, so it does not depend on the jobs to build F or other projects. It picks up the F commit from the branch being tested and updates the Nix flake to use it (thanks for the command to do that).

It also uses the magic-cache which saves about 10 minutes of setup.

Some questions I have are: 1- Would it make sense to add separate jobs for its dependencies (comparse, dolev-yao)? They are being built here, of course, but maybe it'd be nicer to have them in separated jobs as dependencies to this one for better visibility in the actions run page. Given the magic-cache I think this should also be just as fast. 2- We should document what to do on a failure here, since I think not everyone has Nix set up. 3- Maybe set --proof_recovery too?

[mtzguido]

Kicking a run here https://github.com/mtzguido/FStar/actions/runs/11150726528

[TWal]

Awesome thank you!

Yes it would make sense to also start something for Comparse and for DY, although some of their code is also compiled by MLS:

• Comparse also runs a series of tests for its tactic (which proved to be a good regression test e.g. when the core typechecker was introduced)
• DY* also verifies example protocols, which may also break

There is the question whether we compile them sequentially (the complete time to build would be longer) or in parallel (the total compute energy used would be greater, if e.g. there is a problem in Comparse). I think in parallel would be better if we can afford the extra compute energy.

If the cache action works well, it could make sense to first build fstar with nix in a separate workflow, and then build Comparse, DY and MLS?

[mtzguido]

Updated by adding Comparse and DY, and a previous F Nix job as a dependency. See https://github.com/mtzguido/FStar/actions/runs/11196024185.

I think the cache does work and F is reused, since the time for these projects decreased by ~10mins each, and I don't see any building of F (like building '/nix/store/d078i8ryigf45q7h1i8af9ka8xyfjv94-fstar-ulib-27387fe8a40875dba04854b071b5050af91a3dc0.drv'... in the log). This previous attempt didn't have the F* caching: https://github.com/mtzguido/FStar/actions/runs/11195828123.

If it makes sense to you @TWal, I can merge this now. It would be useful to have some note about how to fix a failure though. Is it maybe something like 1) getting the repo 2) updating F* flake as above 3) nix develop?

[TWal]

It looks good, thanks!

I think the procedure you give is correct (just need "4) make check").