tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Add proof checking time to manifest details #123

Open ahelwer opened 8 months ago

ahelwer commented 8 months ago

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.