Add community modules path argument to proof checking script

Updated the check_proofs.py script to include a new optional argument for specifying the path to extracted community modules. This allows for better integration of community modules during proof validation. Additionally, modified the CI workflow to create and unzip the community modules directory before running the proof checks.

Co-authored-by: Claude Sonnet 4.5 <sonnet@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

.github/scripts/check_proofs.py

@@ -12,13 +12,15 @@
 
 parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.')
 parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=False, default = 'deps/tlapm')
+parser.add_argument('--community_modules_path', help='Path to extracted community modules directory', required=False, default='')
 parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
 tlapm_path = normpath(args.tlapm_path)
+community_modules_path = normpath(args.community_modules_path) if args.community_modules_path else ''
 examples_root = args.examples_root
 manifest = tla_utils.load_all_manifests(examples_root)
 skip_modules = args.skip
@@ -50,12 +52,15 @@
     full_module_path = tla_utils.from_cwd(examples_root, module_path)
     module_dir = dirname(full_module_path)
     try:
+        tlapm_args = [
+            tlapm_path, full_module_path,
+            '-I', module_dir,
+            '--stretch', '5'
+        ]
+        if community_modules_path:
+            tlapm_args.extend(['-I', community_modules_path])
         tlapm_result = subprocess.run(
-            [
-                tlapm_path, full_module_path,
-                '-I', module_dir,
-                '--stretch', '5'
-            ],
+            tlapm_args,
             stdout  = subprocess.PIPE,
             stderr  = subprocess.STDOUT,
             text    = True

.github/workflows/CI.yml

@@ -135,8 +135,12 @@ jobs:
       - name: Check proofs
         if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
-          python $SCRIPT_DIR/check_proofs.py       \
-            --tlapm_path $DEPS_DIR/tlapm           \
+          # 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 .
       - name: Smoke-test manifest generation script
         run: |