You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently we manually exclude specific modules from proof checking in the CI because they run too long. Given that proof checking time can have as high of variability as model checking, it makes sense to include data about proof check time in the manifest then use that to determine whether to check the proof in the CI. Possibly we could have a CI workflow scheduled to run weekly which checks these long-running proofs along with the macOS workflow.
Failing proofs can continue to be manually excluded because ideally this repo would not have or accept any specs with failing proofs.
The text was updated successfully, but these errors were encountered:
ahelwer
changed the title
Add theorem checking time to manifest details
Add proof checking time to manifest details
Mar 2, 2024
Currently we manually exclude specific modules from proof checking in the CI because they run too long. Given that proof checking time can have as high of variability as model checking, it makes sense to include data about proof check time in the manifest then use that to determine whether to check the proof in the CI. Possibly we could have a CI workflow scheduled to run weekly which checks these long-running proofs along with the macOS workflow.
Failing proofs can continue to be manually excluded because ideally this repo would not have or accept any specs with failing proofs.
The text was updated successfully, but these errors were encountered: