From 684953e06e3eb85e87a56883af3f73b875ad9d2d Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Mon, 3 Aug 2026 21:44:30 +0300 Subject: [PATCH 1/2] 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 --- .github/workflows/CI.yml | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 14024a57..cf5805ec 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -149,11 +149,38 @@ jobs: | map(select(has("proof"))) # Failing on Linux | map(select(.path != "specifications/LoopInvariance/SumSequence.tla")) + # Proofs with steps that carry no proof; --strict reports these as + # incomplete (exit 11), so they are checked without it below. + | map(select(.path != "specifications/Paxos/Voting.tla")) + | map(select(.path != "specifications/PaxosHowToWinATuringAward/Voting.tla")) + | map(select(.path != "specifications/byzpaxos/PConProof.tla")) + | map(select(.path != "specifications/allocator/AllocatorImplementation_proof.tla")) + | map(select(.path != "specifications/MultiCarElevator/Elevator_proof.tla")) # Skip long-running proofs in CI | map(select(.proof.maxRuntimeMinutes <= 5)) | map((.proof.maxRuntimeMinutes | tostring) + "\u0000" + .path + "\u0000") | join("")' \ | xargs --verbose --null --no-run-if-empty -n 2 \ + sh -c 'time timeout --signal=KILL "${1}m" "$DEPS_DIR/tlapm/bin/tlapm" --strict "$2" -I "$DEPS_DIR/community" --stretch 5' -- + - name: Check proofs with incomplete steps + if: matrix.os != 'windows-latest' && !matrix.unicode + run: | + set -o pipefail + find specifications -iname "manifest.json" -print0 \ + | xargs --null --no-run-if-empty \ + jq --join-output ' + .modules + | map(select(has("proof"))) + | map(select(.proof.maxRuntimeMinutes <= 5)) + | map(select( + .path == "specifications/Paxos/Voting.tla" + or .path == "specifications/PaxosHowToWinATuringAward/Voting.tla" + or .path == "specifications/byzpaxos/PConProof.tla" + or .path == "specifications/allocator/AllocatorImplementation_proof.tla" + or .path == "specifications/MultiCarElevator/Elevator_proof.tla")) + | map((.proof.maxRuntimeMinutes | tostring) + "\u0000" + .path + "\u0000") + | join("")' \ + | xargs --verbose --null --no-run-if-empty -n 2 \ sh -c 'time timeout --signal=KILL "${1}m" "$DEPS_DIR/tlapm/bin/tlapm" "$2" -I "$DEPS_DIR/community" --stretch 5' -- - name: Smoke-test manifest generation script run: | From 930356dbb7eace5d4253a048e90d1ea88b57ee6d Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Tue, 4 Aug 2026 13:32:33 +0300 Subject: [PATCH 2/2] 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 --- .github/workflows/CI.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index cf5805ec..3126e95b 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -151,10 +151,16 @@ jobs: | map(select(.path != "specifications/LoopInvariance/SumSequence.tla")) # Proofs with steps that carry no proof; --strict reports these as # incomplete (exit 11), so they are checked without it below. + # Voting/PConProof: steps left open deliberately. | map(select(.path != "specifications/Paxos/Voting.tla")) | map(select(.path != "specifications/PaxosHowToWinATuringAward/Voting.tla")) | map(select(.path != "specifications/byzpaxos/PConProof.tla")) + # AllocatorImplementation: blocked on referring to facts derived in + # instantiated modules; deferred until that part of the PM is + # reimplemented. | map(select(.path != "specifications/allocator/AllocatorImplementation_proof.tla")) + # Elevator: blocked on the PM not handling definitions of the form + # [x \in S, y \in T |-> e(x,y)]. | map(select(.path != "specifications/MultiCarElevator/Elevator_proof.tla")) # Skip long-running proofs in CI | map(select(.proof.maxRuntimeMinutes <= 5))