Update dependency: deps/k_release (#2572)

* deps/k_release: Set Version 7.1.103 * Set Version: 1.0.678 * kevm-pyk/: sync poetry files pyk version 7.1.103 * flake.{nix,lock}: update Nix derivations * renaming parameters --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimovic <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
runtimeverification · Aug 10, 2024 · 25de575 · 25de575
1 parent 0b75078
commit 25de575
Show file tree

Hide file tree

Showing 10 changed files with 50 additions and 29 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.102
+7.1.103
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,11 +2,11 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.102";
+    k-framework.url = "github:runtimeverification/k/v7.1.103";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/k/v7.1.102?dir=pyk";
+    pyk.url = "github:runtimeverification/k/v7.1.103?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {

diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
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.677"
+version = "1.0.678"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.102"
+kframework = "7.1.103"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

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.677'
+VERSION: Final = '1.0.678'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -301,7 +301,8 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
             kore_rpc_command=kore_rpc_command,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
-            trace_rewrites=options.trace_rewrites,
+            log_succ_rewrites=options.log_succ_rewrites,
+            log_fail_rewrites=options.log_fail_rewrites,
             fallback_on=options.fallback_on,
             interim_simplification=options.interim_simplification,
             no_post_exec_simplify=(not options.post_exec_simplify),
@@ -319,7 +320,12 @@ def create_kcfg_explore() -> KCFGExplore:
                     bug_report_id=bug_report_id,
                     dispatch=dispatch,
                 )
-                cterm_symbolic = CTermSymbolic(client, kevm.definition, trace_rewrites=options.trace_rewrites)
+                cterm_symbolic = CTermSymbolic(
+                    client,
+                    kevm.definition,
+                    log_succ_rewrites=options.log_succ_rewrites,
+                    log_fail_rewrites=options.log_fail_rewrites,
+                )
                 return KCFGExplore(
                     cterm_symbolic,
                     kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas),
@@ -482,7 +488,8 @@ def exec_section_edge(options: SectionEdgeOptions) -> None:
         kore_rpc_command=kore_rpc_command,
         smt_timeout=options.smt_timeout,
         smt_retry_limit=options.smt_retry_limit,
-        trace_rewrites=options.trace_rewrites,
+        log_succ_rewrites=options.log_succ_rewrites,
+        log_fail_rewrites=options.log_fail_rewrites,
         llvm_definition_dir=llvm_definition_dir,
     ) as kcfg_explore:
         node_ids = kcfg_explore.section_edge(

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -300,7 +300,8 @@ def get_argument_type() -> dict[str, Callable]:
 
 
 class RPCOptions(Options):
-    trace_rewrites: bool
+    log_succ_rewrites: bool
+    log_fail_rewrites: bool
     kore_rpc_command: str | None
     use_booster: bool
     fallback_on: list[FallbackReason]
@@ -313,7 +314,8 @@ class RPCOptions(Options):
     @staticmethod
     def default() -> dict[str, Any]:
         return {
-            'trace_rewrites': False,
+            'log_succ_rewrites': True,
+            'log_fail_rewrites': False,
             'kore_rpc_command': None,
             'use_booster': True,
             'fallback_on': [],
@@ -959,8 +961,15 @@ def display_args(self) -> ArgumentParser:
     def rpc_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
         args.add_argument(
-            '--trace-rewrites',
-            dest='trace_rewrites',
+            '--no-log-rewrites',
+            dest='log_succ_rewrites',
+            default=None,
+            action='store_false',
+            help='Do not log traces of any simplification and rewrite rule application.',
+        )
+        args.add_argument(
+            '--log-fail-rewrites',
+            dest='log_fail_rewrites',
             default=None,
             action='store_true',
             help='Log traces of all simplification and rewrite rule applications.',

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -348,7 +348,8 @@ def legacy_explore(
     haskell_log_entries: Iterable[str] = (),
     haskell_threads: int | None = None,
     log_axioms_file: Path | None = None,
-    trace_rewrites: bool = False,
+    log_succ_rewrites: bool = True,
+    log_fail_rewrites: bool = True,
     start_server: bool = True,
     maude_port: int | None = None,
     fallback_on: Iterable[FallbackReason] | None = None,
@@ -377,7 +378,9 @@ def legacy_explore(
             no_post_exec_simplify=no_post_exec_simplify,
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=bug_report_id) as client:
-                cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites)
+                cterm_symbolic = CTermSymbolic(
+                    client, kprint.definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+                )
                 yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id)
     else:
         if port is None:
@@ -396,5 +399,7 @@ def legacy_explore(
         with KoreClient(
             'localhost', port, bug_report=bug_report, bug_report_id=bug_report_id, dispatch=dispatch
         ) as client:
-            cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites)
+            cterm_symbolic = CTermSymbolic(
+                client, kprint.definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+            )
             yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id)
diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.677
+1.0.678