move
move copied to clipboard
move-language
[github] Fix and move prover-inconsistency-test
Fixed broken prover-inconsistency-test CI job and moved it from daily to ci-pre-land as prover-tests, since there seems to be no reason to have it in the daily run instead of the PR related run.
Also cleaned it up, removing Slack references and other dead code.
Motivation
The daily CI tasks fails. This solves half of the problem (by omission), while #301 solves the other half.
Have you read the Contributing Guidelines on pull requests?
Yes.
Test Plan
In addition to this PR's CI tests, the new CI job also succeeds in my repository: https://github.com/villesundell/move/runs/7498332280?check_suite_focus=true
In addition to @awelc & @tnowacki, this might be of interest to @bmwill (CI) and @emmazzz (Prover).
The historic reason why we had it in daily instead of CI were flakes in the DPN verification. But perhaps we can make it the default now? @junkil-park WDYT?
The historic reason why we had it in daily instead of CI were flakes in the DPN verification.
Another reason was that the inconsistency check is 10x ~ 20x slower than the normal run of Prover depending on the timeout limit with the -T option (see https://github.com/diem/diem/pull/7984). The inconsistency check runs Prover after injecting false specs on purpose. Prover often does timeout when the verification of Diem Framework fails. It's not ideal, but we treat timeouts as expected results (= negative verification results) in the inconsistency check.
CI changes LGTM, but i'll leave it to @junkil-park and @wrwg to decide if they want to move this to land blocking
Given the experience with timeouts and flakiness, perhaps we can update this PR so it runs nightly (but this time for real as this seemed to have been broken)?
So, would the next course of action be, that I will move the test back to daily and fix it properly? ( @wrwg & @junkil-park )
So, would the next course of action be, that I will move the test back to daily and fix it properly? ( @wrwg & @junkil-park )
Yes please!
Wondering whether this PR is still relevant. @junkil-park can we get nightly consistency tests back for the prover?
So, would the next course of action be, that I will move the test back to daily and fix it properly? ( @wrwg & @junkil-park ) @villesundell , can the inconsistency test come back to daily?