Simplify kompilation for proof tests

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. <[email protected]>",

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'

kevm-pyk/src/tests/conftest.py

@@ -1,14 +1,12 @@
 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, TempPathFactory
+    from pytest import FixtureRequest, Parser
 
 
 def pytest_addoption(parser: Parser) -> None:
@@ -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',
     )
 
@@ -53,9 +51,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')

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
 
@@ -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)
@@ -121,57 +121,46 @@ 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 / 'kompiled',
-                target=KompileTarget.HASKELL,
-                main_file=self.main_file,
-                main_module=self.main_module_name,
-                syntax_module=self.main_module_name,
-                debug=True,
-            )
+        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 / 'target'
-    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'
-    else:
-        cache_dir.mkdir(parents=True)
-    return cache_dir, cache
+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(kompiled_target_cache: tuple[Path, dict[str, Path]]) -> Callable[[Path], Path]:
+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.
     """
-    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 = target_dir / f'{target.id}.lock'
+        output_dir = target_dir / target.id
+        with SoftFileLock(lock_file):
+            if output_dir.exists():
+                return output_dir
+            return target(output_dir)
 
     return kompile
 
@@ -190,7 +179,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,
@@ -201,11 +192,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)

package/version

@@ -1 +1 @@
-1.0.562
+1.0.563