Improve performance of large lemmas proof suite (#2482)

* kevm-pyk/test_prove: run 8 at a time proofs for lemmas-spec * Set Version: 1.0.600 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jun 12, 2024 · 31bd3d8 · 31bd3d8
1 parent 71a19f1
commit 31bd3d8
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 4 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.599"
+version = "1.0.600"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.599'
+VERSION: Final = '1.0.600'
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -206,20 +206,27 @@ class TParams:
     main_claim_id: str | None
     leaf_number: int | None
     break_on_calls: bool
+    workers: int
 
     def __init__(
-        self, main_claim_id: str | None = None, leaf_number: int | None = None, break_on_calls: bool = False
+        self,
+        main_claim_id: str | None = None,
+        leaf_number: int | None = None,
+        break_on_calls: bool = False,
+        workers: int = 1,
     ) -> None:
         self.main_claim_id = main_claim_id
         self.leaf_number = leaf_number
         self.break_on_calls = break_on_calls
+        self.workers = workers
 
 
 TEST_PARAMS: dict[str, TParams] = {
     'mcd/vat-slip-pass-rough-spec.k': TParams(
         main_claim_id='VAT-SLIP-PASS-ROUGH-SPEC.Vat.slip.pass.rough',
         leaf_number=1,
     ),
+    'functional/lemmas-spec.k': TParams(workers=8),
 }
 
 
@@ -269,6 +276,7 @@ def test_pyk_prove(
         definition_dir = kompiled_target_for(spec_file)
         name = str(spec_file.relative_to(SPEC_DIR))
         break_on_calls = name in TEST_PARAMS and TEST_PARAMS[name].break_on_calls
+        workers = 1 if name not in TEST_PARAMS else TEST_PARAMS[name].workers
         options = ProveOptions(
             {
                 'spec_file': spec_file,
@@ -280,6 +288,7 @@ def test_pyk_prove(
                 'use_booster_dev': use_booster_dev,
                 'bug_report': bug_report,
                 'break_on_calls': break_on_calls,
+                'workers': workers,
             }
         )
         exec_prove(options=options)

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.599
+1.0.600