Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged

Conversation

TWal
Copy link
Contributor

@TWal TWal commented Oct 15, 2024

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

@mtzguido
Copy link
Member

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
Copy link
Member

Hmm seems like MLS* still failed?

@mtzguido
Copy link
Member

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
Copy link
Contributor Author

TWal commented Oct 15, 2024

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
Copy link
Member

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
Copy link
Contributor Author

TWal commented Oct 15, 2024

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
Copy link
Member

ok thanks!

@mtzguido mtzguido force-pushed the twal/only_update_fstar_in_check_world branch from b22ae1a to a35ab1b Compare October 15, 2024 16:55
@mtzguido mtzguido merged commit 6e8b157 into FStarLang:master Oct 15, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants