Added CI step to check proofs

[ahelwer]

I think this is worth including so existing (and future) proofs will be checked. There are a number of proofs that are commented out in the script due to the following issues:

• Fingerprints seemingly ignored for some proofs tlapm#85
• Specs failing proof validation #67

Once these are fixed those comments can be removed. I added a step to cache the proof fingerprints which greatly speeds up checking for proofs that have already been checked.

[ahelwer]

There is very high variance in how long it takes to check the proofs. Possible we could only check the ones that finish very quickly:

specifications/LoopInvariance/Quicksort.tla
Checked proofs in 58.1s
specifications/LoopInvariance/SumSequence.tla
Checked proofs in 308.6s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 1.8s
specifications/MisraReachability/ReachabilityProofs.tla
Checked proofs in 11.9s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 5.5s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.3s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 5.3s
specifications/TwoPhase/TLAPS.tla
Checked proofs in 0.3s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.3s
specifications/bcastByz/bcastByz.tla
Checked proofs in 266.6s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 1.0s
specifications/ewd840/TLAPS.tla
Checked proofs in 0.3s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 1.3s
specifications/lamport_mutex/TLAPS.tla
Checked proofs in 0.3s
specifications/sums_even/TLAPS.tla
Checked proofs in 0.1s
specifications/sums_even/sums_even.tla
Checked proofs in 0.2s

I think they finish quickly no matter what when the fingerprints file is present, so another option is to cache the fingerprint files in between CI runs.

[muenchnerkindl]

Not sure if it's a good idea to check proofs as part of a CI run. As you observed, proof checking can require considerable CPU time. We could indicate modules that have proofs that can be checked fast (similar to the "small models" that TLC is run on), but I'm not sure if it's worth the effort.

[ahelwer]

@muenchnerkindl if I could cache the proof fingerprints would that be useful?

[ahelwer]

@lemmy @muenchnerkindl I think this draft PR is now good to merge if you think it's a good idea

[lemmy]

Let's keep the TLAPS.tla files to prevent parse errors for those users who do not care about proofs, unless the committed TLAPS.tla modules break the CI.

[ahelwer]

@lemmy I tested it out and they don't seem to break the CI; I think maybe they broke with the 1.4.5 TLAPS release which is why I removed them. Oh well added back!