Skip to content

Commit

Permalink
Warn user if an outdated K version is being used (#132)
Browse files Browse the repository at this point in the history
* fixes

* Set Version: 0.1.38

* Addressed PR comments

* fix format

* Set Version: 0.1.40

* extrated _check_k_version function

* Format fix

* removed attribute git from kversion comparison

* custom version comparison

* Set Version: 0.1.45

* Addressed PR comments

* Set Version: 0.1.46

* Update README instructions (#151)

* update readme instructions

* Set Version: 0.1.45

* add resources

---------

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

* refactored _check_versions function

* Set Version: 0.1.47

* format

* Set Version: 0.1.48

* Set Version: 0.1.48

* Addressed PR comments

* Set Version: 0.1.50

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Lisandra Silva <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
  • Loading branch information
4 people authored Nov 6, 2023
1 parent 33a6b63 commit acf81a1
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 3 deletions.
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.49
0.1.50
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kontrol"
version = "0.1.49"
version = "0.1.50"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.49'
VERSION: Final = '0.1.50'
27 changes: 27 additions & 0 deletions src/kontrol/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,12 @@
from argparse import ArgumentParser
from typing import TYPE_CHECKING

import pyk
from kevm_pyk import kdist
from kevm_pyk.cli import node_id_like
from kevm_pyk.utils import arg_pair_of
from pyk.cli.utils import file_path
from pyk.kbuild.utils import KVersion, k_version
from pyk.proof.reachability import APRProof
from pyk.proof.tui import APRProofViewer

Expand Down Expand Up @@ -63,6 +65,8 @@ def main() -> None:
args = parser.parse_args()
logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT)

_check_k_version()

executor_name = 'exec_' + args.command.lower().replace('-', '_')
if executor_name not in globals():
raise AssertionError(f'Unimplemented command: {args.command}')
Expand All @@ -71,6 +75,29 @@ def main() -> None:
execute(**vars(args))


def _check_k_version() -> None:
expected_k_version = KVersion.parse(f'v{pyk.K_VERSION}')
actual_k_version = k_version()

if not _compare_versions(expected_k_version, actual_k_version):
_LOGGER.warning(f'K version {expected_k_version} was expected but K version {actual_k_version} is being used.')


def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool:
if ver1.major != ver2.major or ver1.minor != ver2.minor or ver1.patch != ver2.patch:
return False

if ver1.git == ver2.git:
return True

if ver1.git and ver2.git:
return False

git = ver1.git or ver2.git
assert git # git is not None for exactly one of ver1 and ver2
return not git.ahead and not git.dirty


# Command implementation


Expand Down

0 comments on commit acf81a1

Please sign in to comment.