From bce1dc246bd40eb3391f5671848acce5f820194b Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 10 Apr 2026 22:17:19 -0400 Subject: [PATCH] CI: check proofs using find | jq | xargs bash pipeline Signed-off-by: Andrew Helwer --- .github/workflows/CI.yml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 6999b008..90a311b4 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -135,13 +135,16 @@ jobs: - name: Check proofs if: matrix.os != 'windows-latest' && !matrix.unicode run: | - # Extract community modules for TLAPM - mkdir -p $DEPS_DIR/community/modules - unzip -q -o $DEPS_DIR/community/modules.jar -d $DEPS_DIR/community/modules - python $SCRIPT_DIR/check_proofs.py \ - --tlapm_path $DEPS_DIR/tlapm \ - --community_modules_path $DEPS_DIR/community/modules \ - --examples_root . + set -o pipefail + find specifications -iname "manifest.json" -print0 \ + | xargs --verbose --null --no-run-if-empty \ + jq --join-output \ + '.modules + | map(select(has("proof"))) + | map(.path) + | "\(join("\u0000"))\u0000"' \ + | xargs --verbose --null --no-run-if-empty --replace={TLA_FILE} sh -c \ + '$DEPS_DIR/tlapm/bin/tlapm {TLA_FILE} -I $(dirname {TLA_FILE}) --stretch 5' - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \