Skip to content

Commit

Permalink
Fix temp directory being deleted too early (#2160)
Browse files Browse the repository at this point in the history
* Fix temp directory being deleted too early

* Set Version: 1.0.341

* Fix formatting

* Set Version: 1.0.343

* Update kevm-pyk/src/kevm_pyk/__main__.py

* Set Version: 1.0.348

* Set Version: 1.0.350

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
nwatson22 and devops authored Nov 9, 2023
1 parent 7b04335 commit cc7d175
Show file tree
Hide file tree
Showing 4 changed files with 9 additions and 19 deletions.
2 changes: 1 addition & 1 deletion kevm-pyk/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 = "kevm-pyk"
version = "1.0.349"
version = "1.0.350"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.349'
VERSION: Final = '1.0.350'
22 changes: 6 additions & 16 deletions kevm-pyk/src/kevm_pyk/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -295,7 +295,10 @@ def exec_prove(
_ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}')
md_selector = 'k'

digest_file = save_directory / 'digest' if save_directory is not None else None
if save_directory is None:
save_directory = Path(tempfile.mkdtemp())

digest_file = save_directory / 'digest'

if definition_dir is None:
definition_dir = kdist.get('evm-semantics.haskell')
Expand All @@ -305,9 +308,6 @@ def exec_prove(
if smt_retry_limit is None:
smt_retry_limit = 10

if save_directory is None:
save_directory = Path(tempfile.TemporaryDirectory().name)

kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report)

include_dirs = [Path(include) for include in includes]
Expand Down Expand Up @@ -363,22 +363,12 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
) as kcfg_explore:
proof_problem: Proof
if is_functional(claim):
if (
save_directory is not None
and not reinit
and up_to_date
and EqualityProof.proof_exists(claim.label, save_directory)
):
if not reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory):
proof_problem = EqualityProof.read_proof_data(save_directory, claim.label)
else:
proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory)
else:
if (
save_directory is not None
and not reinit
and up_to_date
and APRProof.proof_data_exists(claim.label, save_directory)
):
if not reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory):
proof_problem = APRProof.read_proof_data(save_directory, claim.label)

else:
Expand Down
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.349
1.0.350

0 comments on commit cc7d175

Please sign in to comment.