Fingerprints seemingly ignored for some proofs

[ahelwer]

Using the 202210041448 release, the following proofs in the tlaplus/examples repo take a long time to check regardless of whether they were previously checked and their fingerprints stored in the .tlacache directory:

specifications/LoopInvariance/Quicksort.tla
specifications/LoopInvariance/SumSequence.tla
specifications/bcastByz/bcastByz.tla

This proof only takes six seconds to check but it still takes six seconds to check even if its fingerprints exist:

specifications/MisraReachability/ReachabilityProofs.tla

To help with differentiation, checking the following proofs is correctly greatly sped up when their fingerprints exist, going from ~10 seconds to ~0.5 seconds:

specifications/LoopInvariance/BinarySearch.tla
specifications/MisraReachability/ReachableProofs.tla
specifications/TeachingConcurrency/SimpleRegular.tla

[lemmy]

Possibly related #84

[ahelwer]

Wow weird coincidence, I had been sitting on this issue for months!

[ahelwer]

Oops reopening because the PR isn't yet merged I guess

[kape1395]

#84 is merged now. Can we close this issue?

[ahelwer]

Probably!