CI: time proofs and skip long-running ones

[ahelwer]

No description provided.

[lemmy]

What's the rational/goal of this PR?

[ahelwer]

Basically make the CI take less time for PRs, but PRs happen relatively rarely so it is perhaps not worth it.

[lemmy]

TLAPS-related PRs are even rarer but do occur occasionally (#211). It would be good if TLAPS could be conditionally activated, or triggered manually.

[ahelwer]

Hmmm, that would be interesting. Only check the proofs on paths touched by the PR, and then check all proofs on push to master (and also tools or TLAPM build).

[ahelwer]

@lemmy I changed this PR to skip specific long-running proofs by name. Are there any other notably long-running proofs we should skip? If there are a large enough number we can change the approach to using the runtime field; jq supports parsing this with the strftime("HH:MM:SS") function.

[lemmy]

specifications/tcp/tcp_proof.tla takes too long to run in CI, so I suggest skipping it by name.

More generally, it is not clear to me what the runtime field is measured against. Is it based on a local machine, GitHub CI, or some specific hardware configuration?

[ahelwer]

It's a very unscientific measurement largely intended to convey the rough order of magnitude of time required to check a proof on average consumer computing hardware (CPU made after 2014 or so, 8 GB+ of RAM). I just think it's nice to know whether I should expect a proof to run in five minutes, fifty minutes, or five hours. That being said if we don't find it that useful it can just be removed.