search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

fix(check-world): only update F* for Comparse, DY* and MLS* #3568

Closed TWal closed 1 month ago

TWal commented 1 month ago

This would prevent having the check-world red when e.g. MLS fails because of a breaking change in DY.

mtzguido commented 1 month ago

Thanks Théophile! Kicking a run here https://github.com/mtzguido/FStar/actions/runs/11347865272

(I should a comment hook so I can just type !check-world...)

mtzguido commented 1 month ago

Hmm seems like MLS* still failed?

mtzguido commented 1 month ago

Oh, maybe just noise?

       > All verification conditions discharged successfully
       > * Error 19 at src/core/DY.Core.Bytes.fst(2189,2-2189,21):
       >   - Assertion failed
       >   - See also Prims.fst(441,83-441,96)
TWal commented 1 month ago

Huh, that's a bit weird, I don't have noise on these proofs usually. Or maybe there is more noise on GitHub's VMs? Will check whether nix is happy on my computer and report back.

mtzguido commented 1 month ago

Or maybe there is more noise on GitHub's VMs?

I haven't observed that, but it's a possibility... or maybe just the recent library reshuffling put this proof over the line?

TWal commented 1 month ago

It looks like it isn't noise, the build also fails on my computer. Seems that F randomly broke an old version on DY that is still used by MLS, but the new DY is fixed for some reason…

Well, the conclusion is that we can merge, MLS* is now fixed.

mtzguido commented 1 month ago

ok thanks!