diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 30c02a0783..02eb3da773 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -14,6 +14,7 @@ from pathlib import Path from typing import TYPE_CHECKING +from filelock import SoftFileLock from pathos.pools import ProcessPool # type: ignore from pyk.cli.pyk import parse_toml_args from pyk.cterm import CTermSymbolic @@ -171,28 +172,29 @@ def digest(self) -> str: return hash_str(f'{claim_hash}{deps_digest}') def up_to_date(self, digest_file: Path | None) -> bool: - if not isinstance(digest_file, Path) or not digest_file.exists(): - return False - digest_dict = json.loads(digest_file.read_text()) - if 'claims' not in digest_dict: - digest_dict['claims'] = {} - digest_file.write_text(json.dumps(digest_dict, indent=4)) - if self.claim.label not in digest_dict['claims']: - return False - return digest_dict['claims'][self.claim.label] == self.digest + with SoftFileLock(f'{digest_file}.lock'): + if not isinstance(digest_file, Path) or not digest_file.exists(): + return False + digest_dict = json.loads(digest_file.read_text()) + if 'claims' not in digest_dict: + return False + if self.claim.label not in digest_dict['claims']: + return False + return digest_dict['claims'][self.claim.label] == self.digest def update_digest(self, digest_file: Path | None) -> None: if digest_file is None: return digest_dict = {} - if digest_file.exists(): - digest_dict = json.loads(digest_file.read_text()) - if 'claims' not in digest_dict: - digest_dict['claims'] = {} - digest_dict['claims'][self.claim.label] = self.digest - digest_file.write_text(json.dumps(digest_dict, indent=4)) + with SoftFileLock(f'{digest_file}.lock'): + if digest_file.exists(): + digest_dict = json.loads(digest_file.read_text()) + if 'claims' not in digest_dict: + digest_dict['claims'] = {} + digest_dict['claims'][self.claim.label] = self.digest + digest_file.write_text(json.dumps(digest_dict, indent=4)) - _LOGGER.info(f'Updated claim {self.claim.label} in digest file: {digest_file}') + _LOGGER.info(f'Updated claim {self.claim.label} in digest file: {digest_file}') def init_claim_jobs(spec_module_name: str, claims: list[KClaim]) -> frozenset[KClaimJob]: diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 5e586fd1f1..c49202a2d5 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -329,7 +329,6 @@ def test_prove_rules( tmp_path: Path, caplog: LogCaptureFixture, no_use_booster: bool, - force_sequential: bool, use_booster_dev: bool, bug_report: BugReport | None, spec_name: str | None, @@ -340,8 +339,8 @@ def test_prove_rules( tmp_path, caplog, no_use_booster, - force_sequential, - use_booster_dev, + force_sequential=True, + use_booster_dev=use_booster_dev, bug_report=bug_report, spec_name=spec_name, ) @@ -358,7 +357,6 @@ def test_prove_functional( tmp_path: Path, caplog: LogCaptureFixture, no_use_booster: bool, - force_sequential: bool, use_booster_dev: bool, bug_report: BugReport | None, spec_name: str | None, @@ -369,8 +367,8 @@ def test_prove_functional( tmp_path, caplog, no_use_booster, - force_sequential, - use_booster_dev, + force_sequential=True, + use_booster_dev=use_booster_dev, bug_report=bug_report, spec_name=spec_name, workers=8, @@ -381,7 +379,6 @@ def test_prove_dss( kompiled_target_for: Callable[[Path], Path], tmp_path: Path, caplog: LogCaptureFixture, - force_sequential: bool, bug_report: BugReport | None, ) -> None: for spec_file in [REPO_ROOT / 'tests/specs/mcd/vat-spec.k', REPO_ROOT / 'tests/specs/mcd-structured/vat-spec.k']: @@ -390,9 +387,9 @@ def test_prove_dss( kompiled_target_for, tmp_path, caplog, - False, - force_sequential, - False, + no_use_booster=False, + force_sequential=True, + use_booster_dev=False, bug_report=bug_report, spec_name=None, workers=8,