Fix proofs

[muenchnerkindl]

I went over all examples that contain proofs and made sure that they run with the current version of TLAPS, on both Linux and MacOS. Unfortunately, the CI terminates with error because of the use of an obsolete version of artefacts but after staring at CI.yml and some of the scripts, I still don't see where that happens.

[lemmy]

Can you rebase on top of 1408f6c?

[ahelwer]

(Have to search for ERROR:root in log to see error since there is quite a bit of non error output)

INFO:root:specifications\ewd840\EWD840.cfg in 1.4s vs. 1s expected
2025-07-01T11:31:25.9099469Z ERROR:root:Recorded state count info differed from actual state counts:
2025-07-01T11:31:25.9100193Z ERROR:root:(distinct/total/depth); expected: (302, 2001, 9), actual: (302, 1, 9)

[ahelwer]

This might be a bug with the validation code since the state counts look to be correct in the output. I will take a look this morning.

What you can do is comment out all the validation steps in the CI other than the proofs, make sure those work, then un-comment the validation steps. Sorry for all the unnecessary work!!

[muenchnerkindl]

Thanks! Indeed I was going to ask you for help since (302, 1, 9) makes no sense so there must be an issue with the regex matcher (but it looked good to me). Moreover I didn't touch this part ... Will try to focus on proof checking now.

[ahelwer]

The cause seems to be that something is causing SANY to print out "2,001 states generated" instead of "2001 states generated", which breaks the regex. Per Java's printf docs, this can be specific to the user locale. So something about the locale on the github CI runners is causing it. Regardless, I will improve the regex so it accepts commas.

[ahelwer]

Okay the state count number issue is fixed and merged into master. Unfortunately it required updating existing state counts in the manifest (which were wrong for the same reason!) so there will likely be merge conflicts.

[muenchnerkindl]

Finally, all proofs are checked on the GitHub servers, after adding a stretch factor of 5. The longest-running proofs are already excluded from CI, but we could also exclude ewd998/EWD998_proof and lamport_mutex/LamportMutex_proofs since they also take quite long.

@ahelwer: I didn't rebase on your fix for the state count regex because the CI run is flagged as failed.

[ahelwer]

Thanks for all the amazing work, @muenchnerkindl! Would you like me to handle all the rebasing & conflicts and stuff or do you want to do it? It gets substantially easier if you squash all your commits into one first.

[muenchnerkindl]

Thanks @ahelwer! I tried to rebase but there was an issue with a commit missing sign-off, and then I was traveling. I'll try once more tomorrow.