Closed gebner closed 9 months ago
Some of the tests still fail however, e.g. Z3 fails to show that the invariant is preserved in
invariantDecl_MaintainedIfStmtSatisfies
.
FWIW, this test (as well as a few other ones) already fail on the main
branch.
Some of the tests still fail however, e.g. Z3 fails to show that the invariant is preserved in
invariantDecl_MaintainedIfStmtSatisfies
.FWIW, this test (as well as a few other ones) already fail on the
main
branch.
As I understand, the fst files (mostly generated) in the Tests
folder are still unstable and it's fine they are failing. The files in the lib
folder should be verified without any problem.
Also, I'm not sure if we can backport the changes to our development repo, as we would prefer a stable fstar version for benchmarking, etc. But the changes doesn't seem to complicated and maybe we can just merge every time we are pushing to the main branch here.
we would prefer a stable fstar version for benchmarking, etc.
Would it be okay to track the latest F* release instead, or are you looking for longer-term stability? They come out every couple of months (last one was actually on Saturday).
Yes, tracking the latest F release would be preferable to tracking the nightly F version. Is that OK?
Yes, that's great. We can make a branch if we need further changes to support nightly F*, but that's going to be a much smaller delta. Starmada was three releases worth of breaking changes behind.
For our upcoming F dataset, we want to build all F projects with the same, nightly F version. This PR makes the changes necessary to build with the latest and greatest F.
Some of the tests still fail however, e.g. Z3 fails to show that the invariant is preserved in
invariantDecl_MaintainedIfStmtSatisfies
.