From 94c3adcaf30871f677da30d4b9a3ab85a0655484 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Fri, 31 Jul 2026 20:05:33 +0300 Subject: [PATCH] ci: pass --strict when verifying TLAPS proofs 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 --- .github/workflows/main.yml | 2 +- .github/workflows/pr.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f681fb8..c658627 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -131,7 +131,7 @@ jobs: status=0 for proof in *_proofs.tla; do echo "::group::Verifying $proof" - tlapm --cleanfp "$proof" || status=1 + tlapm --strict --cleanfp "$proof" || status=1 echo "::endgroup::" done exit $status diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index b3d0a7a..48d70a2 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -55,7 +55,7 @@ jobs: status=0 for proof in *_proofs.tla; do echo "::group::Verifying $proof" - tlapm --cleanfp "$proof" || status=1 + tlapm --strict --cleanfp "$proof" || status=1 echo "::endgroup::" done exit $status