diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py index 1bce4442..e213d6c7 100644 --- a/.github/scripts/check_proofs.py +++ b/.github/scripts/check_proofs.py @@ -4,51 +4,40 @@ from argparse import ArgumentParser from os.path import dirname, join, normpath +import logging import subprocess from timeit import default_timer as timer import tla_utils +logging.basicConfig(level=logging.INFO) + 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=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[]) args = parser.parse_args() tlapm_path = normpath(args.tlapm_path) manifest_path = normpath(args.manifest_path) manifest = tla_utils.load_json(manifest_path) examples_root = dirname(manifest_path) - -# Tracked in https://github.com/tlaplus/Examples/issues/67 -failing_proofs = [ - 'specifications/Bakery-Boulangerie/Bakery.tla', - 'specifications/Bakery-Boulangerie/Boulanger.tla', - 'specifications/Paxos/Consensus.tla', - 'specifications/PaxosHowToWinATuringAward/Consensus.tla', - 'specifications/lamport_mutex/LamportMutex_proofs.tla', - 'specifications/ewd998/EWD998_proof.tla' -] - -# Fingerprint issues; tracked in https://github.com/tlaplus/tlapm/issues/85 -long_running_proofs = [ - 'specifications/LoopInvariance/Quicksort.tla', - 'specifications/LoopInvariance/SumSequence.tla', - 'specifications/bcastByz/bcastByz.tla', - 'specifications/MisraReachability/ReachabilityProofs.tla' -] +skip_modules = [normpath(path) for path in args.skip] proof_module_paths = [ module['path'] for spec in manifest['specifications'] for module in spec['modules'] - if 'proof' in module['features'] - and module['path'] not in failing_proofs - and module['path'] not in long_running_proofs + if 'proof' in module['features'] + and normpath(module['path']) not in skip_modules ] +for path in skip_modules: + logging.info(f'Skipping {path}') + success = True tlapm_path = join(tlapm_path, 'bin', 'tlapm') for module_path in proof_module_paths: - print(module_path) + logging.info(module_path) start_time = timer() module_path = tla_utils.from_cwd(examples_root, module_path) module_dir = dirname(module_path) @@ -59,10 +48,10 @@ ], capture_output=True ) end_time = timer() - print(f'Checked proofs in {end_time - start_time:.1f}s') + logging.info(f'Checked proofs in {end_time - start_time:.1f}s') if tlapm.returncode != 0: - print('FAILURE') - print(tlapm.stderr.decode('utf-8')) + logging.error(f'Proof checking failed in {module_path}:') + logging.error(tlapm.stderr.decode('utf-8')) success = False exit(0 if success else 1) diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index f3d5689c..081e1c84 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -16,6 +16,7 @@ parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) args = parser.parse_args() logging.basicConfig(level=logging.INFO) @@ -25,6 +26,7 @@ community_jar_path = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) +skip_models = [normpath(path) for path in args.skip] def check_model(module_path, model, expected_runtime): module_path = tla_utils.from_cwd(examples_root, module_path) @@ -68,12 +70,17 @@ def check_model(module_path, model, expected_runtime): (module['path'], model, tla_utils.parse_timespan(model['runtime'])) for spec in manifest['specifications'] for module in spec['modules'] - for model in module['models'] if model['size'] == 'small' + for model in module['models'] + if model['size'] == 'small' + and normpath(model['path']) not in skip_models ], key = lambda m: m[2], reverse=True ) +for path in skip_models: + logging.info(f'Skipping {path}') + success = all([check_model(*model) for model in small_models]) exit(0 if success else 1) diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py index e1fbbb17..7fd69c06 100644 --- a/.github/scripts/parse_modules.py +++ b/.github/scripts/parse_modules.py @@ -15,14 +15,17 @@ parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[]) args = parser.parse_args() +logging.basicConfig(level=logging.INFO) + tools_jar_path = normpath(args.tools_jar_path) tlaps_modules = normpath(args.tlapm_lib_path) community_modules = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -logging.basicConfig(level=logging.INFO) +skip_modules = [normpath(path) for path in args.skip] def parse_module(path): """ @@ -45,20 +48,17 @@ def parse_module(path): manifest = tla_utils.load_json(manifest_path) -# Skip these specs and modules as they do not currently parse -skip_specs = [ - # https://github.com/tlaplus/Examples/issues/66 - 'specifications/ewd998' -] -skip_modules = [] - # List of all modules to parse and whether they should use TLAPS imports modules = [ tla_utils.from_cwd(examples_root, module['path']) - for spec in manifest['specifications'] if spec['path'] not in skip_specs - for module in spec['modules'] if module['path'] not in skip_modules + for spec in manifest['specifications'] + for module in spec['modules'] + if normpath(module['path']) not in skip_modules ] +for path in skip_modules: + logging.info(f'Skipping {path}') + # Parse specs in parallel thread_count = cpu_count() logging.info(f'Parsing using {thread_count} threads') diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py index de08cc3d..38792ff3 100644 --- a/.github/scripts/smoke_test_large_models.py +++ b/.github/scripts/smoke_test_large_models.py @@ -16,6 +16,7 @@ parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) args = parser.parse_args() tools_jar_path = normpath(args.tools_jar_path) @@ -23,6 +24,7 @@ community_jar_path = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) +skip_models = [normpath(path) for path in args.skip] def check_model(module_path, model): module_path = tla_utils.from_cwd(examples_root, module_path) @@ -59,23 +61,18 @@ def check_model(module_path, model): manifest = tla_utils.load_json(manifest_path) -skip_models = [ - # SimKnuthYao requires certain number of states to have been generated - # before termination or else it fails. This makes it not amenable to - # smoke testing. - 'specifications/KnuthYao/SimKnuthYao.cfg', - # SimTokenRing does not work on Windows systems. -] + (['specifications/ewd426/SimTokenRing.cfg'] if os.name == 'nt' else []) - large_models = [ (module['path'], model) for spec in manifest['specifications'] for module in spec['modules'] for model in module['models'] if model['size'] != 'small' - and model['path'] not in skip_models + and normpath(model['path']) not in skip_models ] +for path in skip_models: + logging.info(f'Skipping {path}') + success = all([check_model(*model) for model in large_models]) exit(0 if success else 1) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 34d1ad5a..8a2eb8bf 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -150,17 +150,41 @@ jobs: --manifest_path manifest.json - name: Smoke-test large models run: | + # SimKnuthYao requires certain number of states to have been generated + # before termination or else it fails. This makes it not amenable to + # smoke testing. + SKIP=("specifications/KnuthYao/SimKnuthYao.cfg") + # SimTokenRing does not work on Windows systems. + if [[ "${{ runner.os }}" == "Windows" ]]; then + SKIP+=("specifications/ewd426/SimTokenRing.cfg") + fi python $SCRIPT_DIR/smoke_test_large_models.py \ --tools_jar_path deps/tools/tla2tools.jar \ --tlapm_lib_path deps/tlapm/library \ --community_modules_jar_path deps/community/modules.jar \ - --manifest_path manifest.json + --manifest_path manifest.json \ + --skip "${SKIP[@]}" - name: Check proofs if: matrix.os != 'windows-latest' run: | + SKIP=( + # Failing; see https://github.com/tlaplus/Examples/issues/67 + specifications/Bakery-Boulangerie/Bakery.tla + specifications/Bakery-Boulangerie/Boulanger.tla + specifications/Paxos/Consensus.tla + specifications/PaxosHowToWinATuringAward/Consensus.tla + specifications/lamport_mutex/LamportMutex_proofs.tla + specifications/ewd998/EWD998_proof.tla + # Long-running; see https://github.com/tlaplus/tlapm/issues/85 + specifications/LoopInvariance/Quicksort.tla + specifications/LoopInvariance/SumSequence.tla + specifications/bcastByz/bcastByz.tla + specifications/MisraReachability/ReachabilityProofs.tla + ) python $SCRIPT_DIR/check_proofs.py \ --tlapm_path deps/tlapm-install \ - --manifest_path manifest.json + --manifest_path manifest.json \ + --skip "${SKIP[@]}" - name: Smoke-test manifest generation script run: | rm -r deps/tree-sitter-tlaplus/build