The problem is that checking ReachableProofs.tla erases the saved fingerprints of ReachabilityProofs.tla. More generally, when checking the proofs for one file, tlapm may have to parse other files that contain proofs. Those proofs are not re-checked because tlapm only checks the proofs inside the files that are explicitly given on the command line. Here, the proofs are not checked, but the (empty) fingerprint set is still written to disk, erasing the existing fingerprints.
This bug was introduced in 1938a789 by the fix for another bug.
This is a fix for the problem reported here: https://github.com/tlaplus/Examples/issues/67#issuecomment-1456803312
The problem is that checking
ReachableProofs.tlaerases the saved fingerprints ofReachabilityProofs.tla. More generally, when checking the proofs for one file,tlapmmay have to parse other files that contain proofs. Those proofs are not re-checked becausetlapmonly checks the proofs inside the files that are explicitly given on the command line. Here, the proofs are not checked, but the (empty) fingerprint set is still written to disk, erasing the existing fingerprints.This bug was introduced in 1938a789 by the fix for another bug.