Skip to content

Manifest: added proof runtimes#187

Merged
ahelwer merged 1 commit into
tlaplus:masterfrom
ahelwer:proof-runtime
Aug 22, 2025
Merged

Manifest: added proof runtimes#187
ahelwer merged 1 commit into
tlaplus:masterfrom
ahelwer:proof-runtime

Conversation

@ahelwer
Copy link
Copy Markdown
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
Copy Markdown
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 <ahelwer@pm.me>
@ahelwer
Copy link
Copy Markdown
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