|
3 | 3 | """ |
4 | 4 |
|
5 | 5 | from argparse import ArgumentParser |
| 6 | +from datetime import timedelta |
6 | 7 | from os.path import dirname, join, normpath |
7 | 8 | import logging |
8 | 9 | import subprocess |
9 | 10 | from timeit import default_timer as timer |
10 | 11 | import tla_utils |
11 | 12 |
|
12 | 13 | parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.') |
13 | | -parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=True) |
14 | | -parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True) |
| 14 | +parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=False, default = 'deps/tlapm') |
| 15 | +parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.') |
| 16 | +parser.add_argument('--runtime_seconds_limit', help='Only run proofs with expected runtime less than this value', required=False, default=60) |
15 | 17 | parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[]) |
16 | 18 | parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[]) |
17 | 19 | parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') |
|
22 | 24 | manifest = tla_utils.load_all_manifests(examples_root) |
23 | 25 | skip_modules = args.skip |
24 | 26 | only_modules = args.only |
| 27 | +hard_timeout_in_seconds = args.runtime_seconds_limit * 2 |
25 | 28 |
|
26 | 29 | logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) |
27 | 30 |
|
28 | | -proof_module_paths = [ |
29 | | - module['path'] |
30 | | - for path, spec in manifest |
31 | | - for module in spec['modules'] |
32 | | - if 'proof' in module['features'] |
33 | | - and module['path'] not in skip_modules |
34 | | - and (only_modules == [] or module['path'] in only_modules) |
35 | | -] |
| 31 | +proof_module_paths = sorted( |
| 32 | + [ |
| 33 | + (manifest_dir, spec, module, runtime) |
| 34 | + for manifest_dir, spec in manifest |
| 35 | + for module in spec['modules'] |
| 36 | + if 'proof' in module |
| 37 | + and (runtime := tla_utils.parse_timespan(module['proof']['runtime'])) < timedelta(seconds = args.runtime_seconds_limit) |
| 38 | + and module['path'] not in skip_modules |
| 39 | + and (only_modules == [] or module['path'] in only_modules) |
| 40 | + ], |
| 41 | + key = lambda m : m[3] |
| 42 | +) |
36 | 43 |
|
37 | 44 | for path in skip_modules: |
38 | 45 | logging.info(f'Skipping {path}') |
39 | 46 |
|
40 | 47 | success = True |
41 | 48 | tlapm_path = join(tlapm_path, 'bin', 'tlapm') |
42 | | -for module_path in proof_module_paths: |
| 49 | +for manifest_dir, spec, module, expected_runtime in proof_module_paths: |
| 50 | + module_path = module['path'] |
43 | 51 | logging.info(module_path) |
44 | 52 | start_time = timer() |
45 | | - module_path = tla_utils.from_cwd(examples_root, module_path) |
46 | | - module_dir = dirname(module_path) |
47 | | - tlapm = subprocess.run( |
| 53 | + full_module_path = tla_utils.from_cwd(examples_root, module_path) |
| 54 | + module_dir = dirname(full_module_path) |
| 55 | + tlapm_result = subprocess.run( |
48 | 56 | [ |
49 | | - tlapm_path, module_path, |
| 57 | + tlapm_path, full_module_path, |
50 | 58 | '-I', module_dir, |
51 | 59 | '--stretch', '5' |
52 | 60 | ], |
53 | | - stdout=subprocess.PIPE, |
54 | | - stderr=subprocess.STDOUT, |
55 | | - text=True |
| 61 | + stdout = subprocess.PIPE, |
| 62 | + stderr = subprocess.STDOUT, |
| 63 | + text = True, |
| 64 | + timeout = hard_timeout_in_seconds |
56 | 65 | ) |
57 | 66 | end_time = timer() |
58 | | - logging.info(f'Checked proofs in {end_time - start_time:.1f}s') |
59 | | - if tlapm.returncode != 0: |
60 | | - logging.error(f'Proof checking failed in {module_path}:') |
61 | | - logging.error(tlapm.stdout) |
62 | | - success = False |
63 | | - else: |
64 | | - logging.debug(tlapm.stdout) |
| 67 | + actual_runtime = timedelta(seconds = end_time - start_time) |
| 68 | + match tlapm_result: |
| 69 | + case subprocess.CompletedProcess(): |
| 70 | + output = ' '.join(tlapm_result.args) + '\n' + tlapm_result.stdout |
| 71 | + logging.info(f'Checked proofs in {tla_utils.format_timespan(actual_runtime)} vs. {tla_utils.format_timespan(expected_runtime)} expected') |
| 72 | + if tlapm_result.returncode != 0: |
| 73 | + logging.error(f'Proof checking failed for {module_path}:') |
| 74 | + logging.error(output) |
| 75 | + success = False |
| 76 | + else: |
| 77 | + if 'proof' not in module or module['proof']['runtime'] == 'unknown': |
| 78 | + module['proof'] = { 'runtime' : tla_utils.format_timespan(actual_runtime) } |
| 79 | + manifest_path = join(manifest_dir, 'manifest.json') |
| 80 | + tla_utils.write_json(spec, manifest_path) |
| 81 | + logging.debug(output) |
| 82 | + case subprocess.TimeoutExpired(): |
| 83 | + logging.error(f'{module_path} hit hard timeout of {hard_timeout_in_seconds} seconds') |
| 84 | + args, _ = tlapm_result.args |
| 85 | + output = ' '.join(args) + '\n' + tlapm_result.stdout |
| 86 | + logging.error(output) |
| 87 | + success = False |
| 88 | + case _: |
| 89 | + logging.error(f'Unhandled TLAPM result type {type(tlapm_result)}: {tlapm_result}') |
| 90 | + success = False |
65 | 91 |
|
66 | 92 | exit(0 if success else 1) |
67 | 93 |
|
0 commit comments