From 0b6d468e9fd3ecf880ebcd1db29797e5820e4c0c Mon Sep 17 00:00:00 2001 From: Palina Tolmach Date: Sat, 11 Nov 2023 21:41:54 +0800 Subject: [PATCH] Update options: improve help for `view/show-kcfg`, refactor `rpc_args` (#2161) * Move `use-booster`, `kore-rpc-command` to rpc args * Set Version: 1.0.341 * Update help for `view-kcfg`, `show-kcfg` * Set Version: 1.0.342 * Set Version: 1.0.351 * Set Version: 1.0.354 --------- Co-authored-by: devops --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 11 ++--------- kevm-pyk/src/kevm_pyk/cli.py | 22 +++++++++++++++------- package/version | 2 +- 5 files changed, 20 insertions(+), 19 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7f9fbbc897..22a2c03dcb 100644 --- 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.353" +version = "1.0.354" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index b05d4a8af9..2163329b10 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.353' +VERSION: Final = '1.0.354' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 7ce4e000ef..ab324e4e97 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -707,13 +707,6 @@ def parse(s: str) -> list[T]: action='store_true', help='Reinitialize CFGs even if they already exist.', ) - prove_args.add_argument( - '--use-booster', - dest='use_booster', - default=False, - action='store_true', - help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", - ) prune_proof_args = command_parser.add_parser( 'prune-proof', @@ -742,13 +735,13 @@ def parse(s: str) -> list[T]: command_parser.add_parser( 'view-kcfg', - help='Display tree view of CFG', + help='Explore a given proof in the KCFG visualizer.', parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args], ) command_parser.add_parser( 'show-kcfg', - help='Display tree show of CFG', + help='Print the CFG for a given proof.', parents=[ kevm_cli_args.logging_args, kevm_cli_args.k_args, diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index d07c0b6095..167c6e80ff 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -153,10 +153,25 @@ def rpc_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) args.add_argument( '--trace-rewrites', + dest='trace_rewrites', default=False, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) + args.add_argument( + '--kore-rpc-command', + dest='kore_rpc_command', + type=str, + default=None, + help='Custom command to start RPC server', + ) + args.add_argument( + '--use-booster', + dest='use_booster', + default=False, + action='store_true', + help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", + ) return args @cached_property @@ -203,13 +218,6 @@ def explore_args(self) -> ArgumentParser: type=int, help='Number of times to expand the next pending node in the CFG.', ) - args.add_argument( - '--kore-rpc-command', - dest='kore_rpc_command', - type=str, - default=None, - help='Custom command to start RPC server', - ) args.add_argument( '--port', dest='port', diff --git a/package/version b/package/version index e7dc85f0f0..f41cc05d20 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.353 +1.0.354