From eed2d6bb6b0f2eef270994473d5d18325c1f0f15 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Mon, 20 Apr 2026 09:20:12 -0700 Subject: [PATCH] CI: record proof runtime Disable some proofs due to long checking time Signed-off-by: Andrew Helwer --- .github/workflows/CI.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index ddaf2a2d..5c011373 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -144,11 +144,15 @@ jobs: jq --join-output ' .modules | map(select(has("proof"))) + # Failing on Linux | map(select(.path != "specifications/LoopInvariance/SumSequence.tla")) + # Take too long to check in the CI + | map(select(.path != "specifications/byzpaxos/BPConProof.tla")) + | map(select(.path != "specifications/tcp/tcp_proof.tla")) | map(.path + "\u0000") | join("")' \ | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \ - "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5 + time "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5 - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \