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

@ahelwer ahelwer commented Aug 21, 2025

Copy link
Copy Markdown
Collaborator

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

lemmy commented Aug 21, 2025

Copy link
Copy Markdown
Member

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

ahelwer commented Aug 22, 2025

Copy link
Copy Markdown
Collaborator Author

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