CI: check proofs using find | jq | xargs bash pipeline

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

.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 \