Add --strict to fail on incomplete proofs and empty targets - #278
Merged
Conversation
Contributor
|
Thank you for the contribution, looks good to me! Why is this still a draft? |
Member
Author
|
@muenchnerkindl If this PR has your blessing, I’m inclined to merge it into |
lemmy
marked this pull request as ready for review
June 17, 2026 15:58
There was a problem hiding this comment.
Pull request overview
Adds a new --strict mode to TLAPM so CI/scripts don’t silently succeed when (a) proofs are incomplete due to missing/omitted steps, or (b) an explicit target (e.g. --line) selects zero obligations. Under --strict, TLAPM accumulates the “most severe” condition encountered and exits non-zero with a condition-specific code.
Changes:
- Add
--strictCLI flag, parameter plumbing, and strict-mode exit-status accumulation. - Add strict-mode checks for incomplete proofs and empty explicit targets, plus strict handling for failed obligations.
- Add regression tests and user documentation (option + exit codes).
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
src/tlapm_args.ml |
Adds --strict CLI flag and help text. |
src/params.ml |
Introduces strict, exit_status, and severity/target helpers. |
src/params.mli |
Exposes new strict-related params/helpers. |
src/tlapm_lib.ml |
Implements strict checks and exits with accumulated strict status. |
test/cli/cli_tests.ml |
Verifies CLI parsing toggles strict. |
test/bugs/strict_clean_test.tla |
Ensures --strict doesn’t create false positives on clean proofs. |
test/bugs/strict_missing_proof_test.tla |
Regression test for missing proof steps under --strict. |
test/bugs/strict_omitted_proof_test.tla |
Regression test for OMITTED proofs under --strict. |
test/bugs/strict_empty_target_test.tla |
Regression test for empty --line target under --strict. |
doc/web/content/Documentation/Tutorial/Advanced_options.html |
Documents --strict and exit codes. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tlapm exits 0 and prints "All N obligations proved" even when steps have no proof (missing/omitted generate no obligation, tlaplus#271) or when an explicit --line selects nothing (tlaplus#276). This silently hides mistakes in CI and scripts, where there is no IDE to surface them. --strict makes these conditions exit non-zero. When several conditions occur in one run, the most severe code is returned, in this order (most severe first): 3 internal error, 10 failed obligation, 11 incomplete proof, 12 empty target, 0 clean. So a failed obligation (10) outranks an incomplete proof (11), which outranks an empty target (12). Default behavior is unchanged. Addresses Github issues tlaplus#271 and tlaplus#276 tlaplus#271 tlaplus#276 Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
muenchnerkindl
approved these changes
Jun 18, 2026
muenchnerkindl
left a comment
muenchnerkindl
left a comment
Contributor
There was a problem hiding this comment.
Looks good to me.
lemmy
pushed a commit
to tlaplus/CommunityModules
that referenced
this pull request
Jul 31, 2026
tlapm exits 0 even when proof obligations fail, so `|| status=1` never fires and the job reports success over a proof that did not close. The --strict flag (tlaplus/tlapm#278) turns failed obligations, incomplete proofs, and empty targets into distinct non-zero exit codes. All six _proofs.tla modules were run against tlapm 1.6.0-pre both with and without the flag; every module exits 0 either way, so this does not change today's outcome. It makes the job fail if a future change breaks a proof. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
muenchnerkindl
pushed a commit
to tlaplus/Examples
that referenced
this pull request
Aug 3, 2026
* EWD998: close the nine lemmas that were stated without proof EWD998_proof.tla asserted nine lemmas with no proof. Steps carrying no proof generate no obligation, so tlapm reported "All 807 obligations proved" and exited 0, and `--strict` (tlaplus/tlapm#278) exits 11. The six FoldFunctionOnSet* lemmas are now imported from FunctionTheorems, where they are proved. SumIsInt, SumIsNat and SumEqual get structured proofs on top of them, using FS_Subset to carry finiteness from Node to the index set. SumIterate and SumUnion do not go through that way: TLAPS cannot instantiate the second-order op(_,_) against the LAMBDA in Sum. They are proved instead from MapThenSumSetAddElement and MapThenSumSetDisjointUnion in FiniteSetsExtTheorems, whose operator is unary, and which coincide with Sum once the definitions are unfolded. Functions.tla gains SumFunctionOnSet and SumFunction, which FunctionTheorems requires and the vendored copy predates. With tlapm 1.6.0-pre: 851 obligations, all proved, `--strict` exit 0. Runtime rose from roughly one minute to a minute and a half locally, so maxRuntimeMinutes goes from 2 to 4. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com> * Address review: drop the local Functions copy and the now-unused operators Functions.tla here was a subset of the Community Modules version, which is already on the include path, so the local copy is removed. IsAssociativeOn, IsCommutativeOn and IsIdentityOn were only there to state PlusACI, and PlusACI is no longer referenced now that the fold lemmas come from FunctionTheorems. All four are removed; NodeIsFinite stays. 850 obligations, all proved, --strict exit 0. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com> * Drop the Functions.tla entry from the manifest The module was removed in the previous commit but its manifest entry was left behind, so check_manifest_files.py failed on every platform. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com> --------- Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
muenchnerkindl
pushed a commit
to tlaplus/Examples
that referenced
this pull request
Aug 4, 2026
* CI: check proofs with --strict tlapm exits 0 when a proof step carries no proof at all, since such steps generate no obligation. The proof job therefore passes over proofs that did not close. --strict (tlaplus/tlapm#278) reports these as exit 11. Measured against current master: of the 67 proof modules the job runs, 62 are unaffected by the flag. Five exit 11 because they contain steps stated without proof, and are checked without --strict in a separate step so the distinction stays visible rather than silently folded in. specifications/Paxos/Voting.tla specifications/PaxosHowToWinATuringAward/Voting.tla specifications/byzpaxos/PConProof.tla specifications/allocator/AllocatorImplementation_proof.tla specifications/MultiCarElevator/Elevator_proof.tla Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com> * Record why each excluded proof cannot use --strict Per @muenchnerkindl on the PR: the omissions in AllocatorImplementation and Elevator are blocked on prover limitations rather than left open by choice, so note which is which alongside the exclusions. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com> --------- Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
tlapm exits 0 and prints "All N obligations proved" even when steps have no proof (missing/omitted generate no obligation, #271) or when an explicit --line selects nothing (#276). This silently hides mistakes in CI and scripts, where there is no IDE to surface them.
--strict makes these conditions exit non-zero with distinct, severity-ordered codes: 10 failed obligation, 11 incomplete proof, 12 empty target (most severe wins). Default behavior is unchanged.
Addresses Github issues #271 and #276
#271
#276