Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/kontrol/foundry.py
Original file line number Diff line number Diff line change
Expand Up @@ -962,7 +962,7 @@ def resolve_proof_version(

method_status = method.up_to_date(self.digest_file)

if user_specified_version:
if user_specified_version is not None:
_LOGGER.info(f'Using user-specified version {user_specified_version} for test {test}')
if not Proof.proof_data_exists(f'{test}:{user_specified_version}', self.proofs_dir):
raise ValueError(f'The specified version {user_specified_version} of proof {test} does not exist.')
Expand Down
41 changes: 41 additions & 0 deletions src/tests/unit/test_latest_proof_version.py
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
from __future__ import annotations

from pathlib import Path
from types import SimpleNamespace
from typing import TYPE_CHECKING

import pytest
from pyk.proof.proof import Proof

import kontrol.foundry as foundry_module
from kontrol.foundry import Foundry

if TYPE_CHECKING:
Expand Down Expand Up @@ -63,3 +67,40 @@ def test_foundry_latest_proof_version(

# Then
assert latest_version == expected_version


RESOLVE_PROOF_VERSION_DATA: list[tuple[str, int | None, int]] = [
('explicit_zero', 0, 0),
('explicit_nonzero', 2, 2),
('omitted', None, 3),
]


@pytest.mark.parametrize(
'test_id,user_specified_version,expected_version',
RESOLVE_PROOF_VERSION_DATA,
ids=[test_id for test_id, *_ in RESOLVE_PROOF_VERSION_DATA],
)
def test_foundry_resolve_proof_version(
monkeypatch: MonkeyPatch, test_id: str, user_specified_version: int | None, expected_version: int
) -> None:
# Given
test = 'long%path%to%test%DeeplyNestedTest.testWithMultipleVersions()'
method = SimpleNamespace(up_to_date=lambda _digest_file: True)

monkeypatch.setattr(Foundry, '__init__', lambda _: None)
monkeypatch.setattr(Foundry, 'digest_file', Path('digest'))
monkeypatch.setattr(Foundry, 'proofs_dir', Path('proofs'))
monkeypatch.setattr(Foundry, 'list_proof_dir', mock_listdir)
monkeypatch.setattr(Foundry, 'get_contract_and_method', lambda _self, _test: (None, method))
monkeypatch.setattr(foundry_module, 'kontrol_up_to_date', lambda _digest_file: True)

foundry = Foundry() # type: ignore
existing_proofs = mock_listdir(foundry)
monkeypatch.setattr(Proof, 'proof_data_exists', lambda proof_id, _proofs_dir: proof_id in existing_proofs)

# When
version = foundry.resolve_proof_version(test, reinit=False, user_specified_version=user_specified_version)

# Then
assert version == expected_version