Manifest: added proof runtimes

.github/scripts/check_manifest_features.py

@@ -164,15 +164,19 @@ def check_features(parser, queries, manifest, examples_root):
             if parse_err:
                 success = False
                 logging.error(f'Module {module["path"]} contains syntax errors')
-            expected_features = get_tree_features(tree, queries)
+            module_features = get_tree_features(tree, queries)
+            expected_features = module_features - {'proof'}
             actual_features = set(module['features'])
             if expected_features != actual_features:
                 success = False
                 logging.error(
                     f'Module {module["path"]} has incorrect features in manifest; '
                     + f'expected {list(expected_features)}, actual {list(actual_features)}'
                 )
-            expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in expected_features, queries)
+            if 'proof' in module_features and 'proof' not in module:
+                success = False
+                logging.error(f'Module {module["path"]} contains proof but no proof runtime details in manifest')
+            expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in module_features, queries)
             actual_imports = set(module['communityDependencies'])
             if expected_imports != actual_imports:
                 success = False
@@ -192,7 +196,7 @@ def check_features(parser, queries, manifest, examples_root):
 
 if __name__ == '__main__':
     parser = ArgumentParser(description='Checks metadata in manifest.json files against module and model files in repository.')
-    parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+    parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
     args = parser.parse_args()
 
     manifest = tla_utils.load_all_manifests(args.examples_root)

.github/scripts/check_manifest_files.py

@@ -12,7 +12,7 @@
 import tla_utils
 
 parser = ArgumentParser(description='Checks manifests against module and model files in repository.')
-parser.add_argument('--ci_ignore_path', help='Path to the .ciignore file', required=True)
+parser.add_argument('--ci_ignore_path', help='Path to the .ciignore file', required=False, default='./.ciignore')
 args = parser.parse_args()
 
 ci_ignore_path = normpath(args.ci_ignore_path)

.github/scripts/check_manifest_schema.py

@@ -15,7 +15,7 @@
 import tla_utils
 
 parser = ArgumentParser(description='Checks tlaplus/examples manifest.json files against JSON schema file.')
-parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=True)
+parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=False, default='manifest-schema.json')
 args = parser.parse_args()
 
 examples_root = dirname(args.schema_path)

.github/scripts/check_markdown_table.py

@@ -67,15 +67,15 @@ def from_json(path, spec):
         path,
         set(spec['authors']),
         'beginner' in spec['tags'],
-        any([module for module in spec['modules'] if 'proof' in module['features']]),
+        any([module for module in spec['modules'] if 'proof' in module]),
         any([module for module in spec['modules'] if 'pluscal' in module['features']]),
         any([model for module in spec['modules'] for model in module['models'] if model['mode'] != 'symbolic']),
         any([model for module in spec['modules'] for model in module['models'] if model['mode'] == 'symbolic']),
         spec
     )
 
 parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.')
-parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
+parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=False, default='./README.md')
 args = parser.parse_args()
 
 manifest = tla_utils.load_all_manifests(dirname(args.readme_path))

.github/scripts/check_proofs.py

@@ -3,15 +3,17 @@
 """
 
 from argparse import ArgumentParser
+from datetime import timedelta
 from os.path import dirname, join, normpath
 import logging
 import subprocess
 from timeit import default_timer as timer
 import tla_utils
 
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+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('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
+parser.add_argument('--runtime_seconds_limit', help='Only run proofs with expected runtime less than this value', required=False, default=60)
 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')
@@ -22,46 +24,68 @@
 manifest = tla_utils.load_all_manifests(examples_root)
 skip_modules = args.skip
 only_modules = args.only
+hard_timeout_in_seconds = args.runtime_seconds_limit * 2
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
-proof_module_paths = [
-    module['path']
-    for path, spec in manifest
-    for module in spec['modules']
-        if 'proof' in module['features']
-        and module['path'] not in skip_modules
-        and (only_modules == [] or module['path'] in only_modules)
-]
+proof_module_paths = sorted(
+    [
+        (manifest_dir, spec, module, runtime)
+        for manifest_dir, spec in manifest
+        for module in spec['modules']
+        if 'proof' in module
+            and (runtime := tla_utils.parse_timespan(module['proof']['runtime'])) <= timedelta(seconds = args.runtime_seconds_limit)
+            and module['path'] not in skip_modules
+            and (only_modules == [] or module['path'] in only_modules)
+    ],
+    key = lambda m : m[3]
+)
 
 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:
+for manifest_dir, spec, module, expected_runtime in proof_module_paths:
+    module_path = module['path']
     logging.info(module_path)
     start_time = timer()
-    module_path = tla_utils.from_cwd(examples_root, module_path)
-    module_dir = dirname(module_path)
-    tlapm = subprocess.run(
-        [
-            tlapm_path, module_path,
-            '-I', module_dir,
-            '--stretch', '5'
-        ],
-        stdout=subprocess.PIPE,
-        stderr=subprocess.STDOUT,
-        text=True
-    )
-    end_time = timer()
-    logging.info(f'Checked proofs in {end_time - start_time:.1f}s')
-    if tlapm.returncode != 0:
-        logging.error(f'Proof checking failed in {module_path}:')
-        logging.error(tlapm.stdout)
+    full_module_path = tla_utils.from_cwd(examples_root, module_path)
+    module_dir = dirname(full_module_path)
+    try:
+        tlapm_result = subprocess.run(
+            [
+                tlapm_path, full_module_path,
+                '-I', module_dir,
+                '--stretch', '5'
+            ],
+            stdout  = subprocess.PIPE,
+            stderr  = subprocess.STDOUT,
+            text    = True,
+            timeout = hard_timeout_in_seconds
+        )
+        end_time = timer()
+        actual_runtime = timedelta(seconds = end_time - start_time)
+        output = ' '.join(tlapm_result.args) + '\n' + tlapm_result.stdout
+        logging.info(f'Checked proofs in {tla_utils.format_timespan(actual_runtime)} vs. {tla_utils.format_timespan(expected_runtime)} expected')
+        if tlapm_result.returncode != 0:
+            logging.error(f'Proof checking failed for {module_path}:')
+            logging.error(output)
+            success = False
+        else:
+            if 'proof' not in module or module['proof']['runtime'] == 'unknown':
+                module['proof'] = { 'runtime' : tla_utils.format_timespan(actual_runtime) }
+                manifest_path = join(manifest_dir, 'manifest.json')
+                tla_utils.write_json(spec, manifest_path)
+            logging.debug(output)
+    except subprocess.TimeoutExpired as tlapm_result:
+        # stdout is a string on Windows, byte array everywhere else
+        stdout = tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
+        args, timeout = tlapm_result.args
+        logging.error(f'{module_path} hit hard timeout of {timeout} seconds')
+        output = ' '.join(args) + '\n' + stdout
+        logging.error(output)
         success = False
-    else:
-        logging.debug(tlapm.stdout)
 
 exit(0 if success else 1)
 

.github/scripts/check_small_models.py

@@ -13,11 +13,11 @@
 import tla_utils
 
 parser = ArgumentParser(description='Checks all small TLA+ models in the tlaplus/examples repo using TLC.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
-parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
-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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+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 models to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
@@ -78,9 +78,11 @@ def check_model(module, model, expected_runtime):
             logging.debug(output)
             return True
         case TimeoutExpired():
-            args, _ = tlc_result.args
-            output = ' '.join(args) + '\n' + tlc_result.stdout
-            logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds')
+            args, timeout = tlc_result.args
+            # stdout is a string on Windows, byte array everywhere else
+            stdout = tlc_result.stdout if type(tlc_result.stdout) == str else tlc_result.stdout.decode('utf-8')
+            output = ' '.join(args) + '\n' + stdout
+            logging.error(f'{model_path} hit hard timeout of {timeout} seconds')
             logging.error(output)
             return False
         case _:

.github/scripts/format_markdown_table.py

@@ -13,7 +13,7 @@
 from mistletoe.markdown_renderer import MarkdownRenderer
 
 parser = ArgumentParser(description='Formats or modifies the spec table in README.md.')
-parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
+parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=False, default='README.md')
 args = parser.parse_args()
 
 columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']

.github/scripts/generate_manifest.py

@@ -35,9 +35,20 @@ def get_tla_files(examples_root, dir_path):
     Gets paths of all .tla files in the given directory, except for error
     trace specs.
     """
-    return [
-        path for path in glob.glob(f'{dir_path}/**/*.tla', root_dir=examples_root, recursive=True)
+    return sorted(
+        path
+        for path in glob.glob(f'{dir_path}/**/*.tla', root_dir=examples_root, recursive=True)
         if '_TTrace_' not in path
+    )
+
+def get_tla_file_features(examples_root, dir_path, parser, queries):
+    """
+    Gets paths of all .tla files in a given directory, along with their
+    features.
+    """
+    return [
+        (path, get_module_features(examples_root, path, parser, queries))
+        for path in get_tla_files(examples_root, dir_path)
     ]
 
 def get_cfg_files(examples_root, tla_path):
@@ -73,7 +84,7 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
             {
                 'path': tla_utils.to_posix(tla_path),
                 'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
-                'features': sorted(list(get_module_features(examples_root, tla_path, parser, queries))),
+                'features': sorted(list(module_features - {'proof'})),
                 'models': [
                     {
                         'path': tla_utils.to_posix(cfg_path),
@@ -83,8 +94,8 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
                     }
                     for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
                 ]
-            }
-            for tla_path in sorted(get_tla_files(examples_root, spec_path))
+            } | ({'proof' : {'runtime': 'unknown'}} if 'proof' in module_features else {})
+            for tla_path, module_features in get_tla_file_features(examples_root, spec_path, parser, queries)
         ]
     }
 
@@ -107,9 +118,13 @@ def find_corresponding_module(old_module, new_spec):
     return modules[0] if any(modules) else None
 
 def integrate_module_info(old_module, new_module):
-    fields = []
-    for field in fields:
+    required_fields = []
+    for field in required_fields:
         new_module[field] = old_module[field]
+    optional_fields = ['proof']
+    for field in optional_fields:
+        if field in old_module:
+            new_module[field] = old_module[field]
 
 def find_corresponding_model(old_model, new_module):
     models = [

.github/scripts/parse_modules.py

@@ -11,11 +11,11 @@
 import tla_utils
 
 parser = ArgumentParser(description='Parses all TLA+ modules in the tlaplus/examples repo using SANY.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
-parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
-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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+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 parsing', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')

.github/scripts/record_model_state_space.py

@@ -11,10 +11,10 @@
 import tla_utils
 
 parser = ArgumentParser(description='Updates manifest.json with unique & total model states for each small model.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
-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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+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 models to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')

.github/scripts/smoke_test_large_models.py

@@ -13,11 +13,11 @@
 import tla_utils
 
 parser = ArgumentParser(description='Smoke-tests all larger TLA+ models in the tlaplus/examples repo using TLC.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
-parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
-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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+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 models to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')