From ef7520dd1114055d33fccf35c0fd34fd42e5e183 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 May 2024 12:55:35 +0000 Subject: [PATCH 1/5] Simplify folder layout --- kevm-pyk/src/tests/integration/test_prove.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 0935d9126e..0cbfae7430 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -130,7 +130,7 @@ def name(self) -> str: def __call__(self, output_dir: Path) -> Path: with FileLock(str(output_dir) + '.lock'): return kevm_kompile( - output_dir=output_dir / 'kompiled', + output_dir=output_dir, target=KompileTarget.HASKELL, main_file=self.main_file, main_module=self.main_module_name, @@ -144,13 +144,13 @@ def kompiled_target_cache(kompiled_targets_dir: Path) -> tuple[Path, dict[str, P """ Populate the cache of kompiled definitions from an existing file system directory. If the cache is hot, the `kompiled_target_for` fixture will not containt a call to `kompile`, saving an expesive call to the K frontend. """ - cache_dir = kompiled_targets_dir / 'target' + cache_dir = kompiled_targets_dir cache: dict[str, Path] = {} if cache_dir.exists(): # cache dir exists, populate cache for file in cache_dir.iterdir(): if file.is_dir(): # the cache key is the name of the target, which is the filename by-construction. - cache[file.stem] = file / 'kompiled' + cache[file.stem] = file else: cache_dir.mkdir(parents=True) return cache_dir, cache From 09ffe344ee38912f6f8df68dad325de62457a60f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 May 2024 13:20:15 +0000 Subject: [PATCH 2/5] Eliminate `kompiled_target_cache` --- kevm-pyk/src/tests/integration/test_prove.py | 56 +++++++------------- 1 file changed, 18 insertions(+), 38 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 0cbfae7430..91a65b0dba 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -5,7 +5,7 @@ from typing import TYPE_CHECKING, NamedTuple import pytest -from filelock import FileLock +from filelock import SoftFileLock from pyk.prelude.ml import is_top from pyk.proof.reachability import APRProof @@ -121,57 +121,37 @@ class Target(NamedTuple): main_module_name: str @property - def name(self) -> str: + def id(self) -> str: """ - Target's name is the two trailing path segments and the main module name + The target's id is the two trailing path segments and the main module name """ return f'{self.main_file.parts[-2]}-{self.main_file.stem}-{self.main_module_name}' def __call__(self, output_dir: Path) -> Path: - with FileLock(str(output_dir) + '.lock'): - return kevm_kompile( - output_dir=output_dir, - target=KompileTarget.HASKELL, - main_file=self.main_file, - main_module=self.main_module_name, - syntax_module=self.main_module_name, - debug=True, - ) - - -@pytest.fixture(scope='module') -def kompiled_target_cache(kompiled_targets_dir: Path) -> tuple[Path, dict[str, Path]]: - """ - Populate the cache of kompiled definitions from an existing file system directory. If the cache is hot, the `kompiled_target_for` fixture will not containt a call to `kompile`, saving an expesive call to the K frontend. - """ - cache_dir = kompiled_targets_dir - cache: dict[str, Path] = {} - if cache_dir.exists(): # cache dir exists, populate cache - for file in cache_dir.iterdir(): - if file.is_dir(): - # the cache key is the name of the target, which is the filename by-construction. - cache[file.stem] = file - else: - cache_dir.mkdir(parents=True) - return cache_dir, cache + return kevm_kompile( + output_dir=output_dir, + target=KompileTarget.HASKELL, + main_file=self.main_file, + main_module=self.main_module_name, + syntax_module=self.main_module_name, + debug=True, + ) @pytest.fixture(scope='module') -def kompiled_target_for(kompiled_target_cache: tuple[Path, dict[str, Path]]) -> Callable[[Path], Path]: +def kompiled_target_for(kompiled_targets_dir: Path) -> Callable[[Path], Path]: """ Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec. """ - cache_dir, cache = kompiled_target_cache def kompile(spec_file: Path) -> Path: target = _target_for_spec(spec_file) - - if target.name not in cache: - output_dir = cache_dir / target.name - output_dir.mkdir(exist_ok=True) - cache[target.name] = target(output_dir) - - return cache[target.name] + lock_file = kompiled_targets_dir / f'{target.id}.lock' + output_dir = kompiled_targets_dir / target.id + with SoftFileLock(lock_file): + if output_dir.exists(): + return output_dir + return target(output_dir) return kompile From e03598d46e78ada87396b2eeba18164a627aff3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 May 2024 13:38:30 +0000 Subject: [PATCH 3/5] Make `kompiled_targets_dir` optional --- kevm-pyk/src/tests/conftest.py | 10 +++------- kevm-pyk/src/tests/integration/test_prove.py | 19 +++++++++---------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py index fc675227f8..a160215567 100644 --- a/kevm-pyk/src/tests/conftest.py +++ b/kevm-pyk/src/tests/conftest.py @@ -8,7 +8,7 @@ if TYPE_CHECKING: from pathlib import Path - from pytest import FixtureRequest, Parser, TempPathFactory + from pytest import FixtureRequest, Parser def pytest_addoption(parser: Parser) -> None: @@ -53,9 +53,5 @@ def spec_name(request: FixtureRequest) -> str | None: @pytest.fixture(scope='session') -def kompiled_targets_dir(request: FixtureRequest, tmp_path_factory: TempPathFactory) -> Path: - dir = request.config.getoption('--kompiled-targets-dir') - if dir: - return dir - else: - return tmp_path_factory.mktemp('prekompiled') +def kompiled_targets_dir(request: FixtureRequest) -> Path | None: + return request.config.getoption('--kompiled-targets-dir') diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 91a65b0dba..e16f461aaf 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -23,7 +23,7 @@ from typing import Any, Final from pyk.utils import BugReport - from pytest import FixtureRequest, LogCaptureFixture + from pytest import LogCaptureFixture, TempPathFactory sys.setrecursionlimit(10**8) @@ -139,15 +139,16 @@ def __call__(self, output_dir: Path) -> Path: @pytest.fixture(scope='module') -def kompiled_target_for(kompiled_targets_dir: Path) -> Callable[[Path], Path]: +def kompiled_target_for(tmp_path_factory: TempPathFactory, kompiled_targets_dir: Path | None) -> Callable[[Path], Path]: """ Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec. """ + target_dir = kompiled_targets_dir or tmp_path_factory.mktemp('kompiled') def kompile(spec_file: Path) -> Path: target = _target_for_spec(spec_file) - lock_file = kompiled_targets_dir / f'{target.id}.lock' - output_dir = kompiled_targets_dir / target.id + lock_file = target_dir / f'{target.id}.lock' + output_dir = target_dir / target.id with SoftFileLock(lock_file): if output_dir.exists(): return output_dir @@ -170,7 +171,9 @@ def _target_for_spec(spec_file: Path) -> Target: ALL_TESTS, ids=[str(spec_file.relative_to(SPEC_DIR)) for spec_file in ALL_TESTS], ) -def test_kompile_targets(spec_file: Path, kompiled_target_for: Callable[[Path], Path], request: FixtureRequest) -> None: +def test_kompile_targets( + spec_file: Path, kompiled_target_for: Callable[[Path], Path], kompiled_targets_dir: Path | None +) -> None: """ This test function is intended to be used to pre-kompile all definitions, so that the actual proof tests do not need to do the actual compilation, @@ -181,11 +184,7 @@ def test_kompile_targets(spec_file: Path, kompiled_target_for: Callable[[Path], This test will be skipped if no --kompiled-targets-dir option is given """ - dir = request.config.getoption('--kompiled-targets-dir') - if not dir: - pytest.skip() - - if spec_file in FAILING_BOOSTER_TESTS: + if not kompiled_targets_dir or spec_file in FAILING_BOOSTER_TESTS: pytest.skip() kompiled_target_for(spec_file) From 6e2539ea79a3d08277790f1e65bf11314b7db83e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 May 2024 13:48:57 +0000 Subject: [PATCH 4/5] Create `kompiled_targets_dir` if it does not exist --- kevm-pyk/src/tests/conftest.py | 6 ++---- kevm-pyk/src/tests/integration/test_prove.py | 12 ++++++++++-- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py index a160215567..498f08d1d2 100644 --- a/kevm-pyk/src/tests/conftest.py +++ b/kevm-pyk/src/tests/conftest.py @@ -1,13 +1,11 @@ from __future__ import annotations +from pathlib import Path from typing import TYPE_CHECKING import pytest -from pyk.cli.utils import dir_path if TYPE_CHECKING: - from pathlib import Path - from pytest import FixtureRequest, Parser @@ -32,7 +30,7 @@ def pytest_addoption(parser: Parser) -> None: ) parser.addoption( '--kompiled-targets-dir', - type=dir_path, + type=Path, help='Use pre-kompiled definitions for proof tests', ) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index e16f461aaf..a31294d4f6 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -139,11 +139,19 @@ def __call__(self, output_dir: Path) -> Path: @pytest.fixture(scope='module') -def kompiled_target_for(tmp_path_factory: TempPathFactory, kompiled_targets_dir: Path | None) -> Callable[[Path], Path]: +def target_dir(kompiled_targets_dir: Path | None, tmp_path_factory: TempPathFactory) -> Path: + if kompiled_targets_dir: + kompiled_targets_dir.mkdir(parents=True, exist_ok=True) + return kompiled_targets_dir + + return tmp_path_factory.mktemp('kompiled') + + +@pytest.fixture(scope='module') +def kompiled_target_for(target_dir: Path) -> Callable[[Path], Path]: """ Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec. """ - target_dir = kompiled_targets_dir or tmp_path_factory.mktemp('kompiled') def kompile(spec_file: Path) -> Path: target = _target_for_spec(spec_file) From 75fcb37c47bb972d87f25f353fb107125dc77f94 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 20 May 2024 13:35:22 +0000 Subject: [PATCH 5/5] Set Version: 1.0.563 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 91350ccf1e..6b6cf68036 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.562" +version = "1.0.563" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 61809218c8..689ccd96f1 100644 --- 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.562' +VERSION: Final = '1.0.563' diff --git a/package/version b/package/version index 79de68202a..7858c7eb9d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.562 +1.0.563