Skip to content

Commit c281e53

Browse files
committed
CI: record proof runtime
Disable BPConProof due to long checking time Signed-off-by: Andrew Helwer <ahelwer@pm.me>
1 parent 3a6b92c commit c281e53

1 file changed

Lines changed: 4 additions & 1 deletion

File tree

.github/workflows/CI.yml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,11 +144,14 @@ jobs:
144144
jq --join-output '
145145
.modules
146146
| map(select(has("proof")))
147+
# Failing on Linux
147148
| map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
149+
# Takes 30 minutes to check
150+
| map(select(.path != "specifications/byzpaxos/BPConProof.tla"))
148151
| map(.path + "\u0000")
149152
| join("")' \
150153
| xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
151-
"$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
154+
time "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
152155
- name: Smoke-test manifest generation script
153156
run: |
154157
python $SCRIPT_DIR/generate_manifest.py \

0 commit comments

Comments
 (0)