From 66c2a0f9dc1f7ab82fdade4a1643e7e349316b19 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 Unzip Community Modules for TLAPM Signed-off-by: Andrew Helwer --- .github/scripts/linux-setup.sh | 1 + .github/workflows/CI.yml | 18 +++++++++++------- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh index dbe729eb..419ab3d3 100755 --- a/.github/scripts/linux-setup.sh +++ b/.github/scripts/linux-setup.sh @@ -50,6 +50,7 @@ main() { mkdir -p "$DEPS_DIR/community" wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \ -O "$DEPS_DIR/community/modules.jar" + unzip "$DEPS_DIR/community/modules.jar" -d "$DEPS_DIR/community" # Get TLAPS modules wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR" diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 6999b008..cf626601 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -135,13 +135,17 @@ 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 --null --no-run-if-empty \ + jq --join-output ' + .modules + | map(select(has("proof"))) + | map(select(.path != "specifications/LoopInvariance/SumSequence.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 - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \