Add --maintenance-rate option (#2563)

* Add --maintenance-rate option

* Try to revert plugin change

* Set Version: 1.0.670

* Fix formatting

* Set Version: 1.0.671

* description adjustment

* storing maintenance rate correctly

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.670"
+version = "1.0.671"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.670'
+VERSION: Final = '1.0.671'

kevm-pyk/src/kevm_pyk/cli.py

@@ -177,6 +177,11 @@ def _create_argument_parser() -> ArgumentParser:
         action='store_true',
         help='Reinitialize CFGs even if they already exist.',
     )
+    prove_args.add_argument(
+        '--max-frontier-parallel',
+        type=int,
+        help='Maximum worker threads to use on a single proof to explore separate branches in parallel.',
+    )
 
     prune_args = command_parser.add_parser(
         'prune',
@@ -370,6 +375,7 @@ class KProveOptions(Options):
     always_check_subsumption: bool
     fast_check_subsumption: bool
     direct_subproof_rules: bool
+    maintenance_rate: int
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -378,6 +384,7 @@ def default() -> dict[str, Any]:
             'always_check_subsumption': True,
             'fast_check_subsumption': False,
             'direct_subproof_rules': False,
+            'maintenance_rate': 1,
         }
 
 
@@ -809,7 +816,7 @@ def kprove_args(self) -> ArgumentParser:
         args.add_argument(
             '--debug-equations',
             type=list_of(str, delim=','),
-            help='Comma-separate list of equations to debug.',
+            help='Comma-separated list of equations to debug.',
         )
         args.add_argument(
             '--always-check-subsumption',
@@ -839,6 +846,13 @@ def kprove_args(self) -> ArgumentParser:
             action='store_true',
             help='For passing subproofs, construct lemmas directly from initial to target state.',
         )
+        args.add_argument(
+            '--maintenance-rate',
+            dest='maintenance_rate',
+            default=1,
+            type=int,
+            help='The number of proof iterations performed between two writes to disk and status bar updates. Note that setting to >1 may result in work being discarded if proof is interrupted.',
+        )
         return args
 
     @cached_property

kevm-pyk/src/kevm_pyk/utils.py

@@ -113,6 +113,7 @@ def run_prover(
     force_sequential: bool = False,
     progress: Progress | None = None,
     task_id: TaskID | None = None,
+    maintenance_rate: int = 1,
 ) -> bool:
     prover: APRProver | ImpliesProver
     try:
@@ -137,7 +138,11 @@ def update_status_bar(_proof: Proof) -> None:
             if force_sequential:
                 prover = create_prover()
                 prover.advance_proof(
-                    proof=proof, max_iterations=max_iterations, fail_fast=fail_fast, callback=update_status_bar
+                    proof=proof,
+                    max_iterations=max_iterations,
+                    fail_fast=fail_fast,
+                    callback=update_status_bar,
+                    maintenance_rate=maintenance_rate,
                 )
             else:
                 parallel_advance_proof(
@@ -147,6 +152,7 @@ def update_status_bar(_proof: Proof) -> None:
                     fail_fast=fail_fast,
                     max_workers=max_frontier_parallel,
                     callback=update_status_bar,
+                    maintenance_rate=maintenance_rate,
                 )
 
         elif type(proof) is EqualityProof:

package/version

@@ -1 +1 @@
-1.0.670
+1.0.671