Skip to content

Conversation

@ahelwer
Copy link
Collaborator

@ahelwer ahelwer commented Aug 21, 2025

Recorded runtime details for all existing proofs

Proofs running longer than 1 minute will not be run in CI

Closes #123

@ahelwer ahelwer force-pushed the proof-runtime branch 2 times, most recently from ee94efa to 74926a3 Compare August 21, 2025 21:24
@lemmy
Copy link
Member

lemmy commented Aug 21, 2025

Have you considered whether this might be related to TLAPS’ timeout pragmas?

Recorded runtime details for all existing proofs

Proofs running longer than 1 minute will not be run in CI

Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Copy link
Collaborator Author

ahelwer commented Aug 22, 2025

Adding a SMTT(30) pragma to one troublesome proof in VoteProof.tla did help it finish under the timeout limit, good idea.

@ahelwer ahelwer merged commit a3ecae1 into tlaplus:master Aug 22, 2025
8 checks passed
@ahelwer ahelwer deleted the proof-runtime branch August 22, 2025 20:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

Add proof checking time to manifest details

2 participants