Skip to content

Commit

Permalink
Merge branch 'master' into test-merge-node-simple
Browse files Browse the repository at this point in the history
  • Loading branch information
palinatolmach authored Nov 12, 2024
2 parents 6da9337 + b642aab commit 40baed2
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 15 deletions.
11 changes: 0 additions & 11 deletions src/kontrol/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@
from pyk.cterm.symbolic import CTermSMTError
from pyk.proof.reachability import APRFailureInfo, APRProof
from pyk.proof.tui import APRProofViewer
from rich.highlighter import NullHighlighter
from rich.logging import RichHandler

from . import VERSION
from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
Expand Down Expand Up @@ -115,15 +113,6 @@ def main() -> None:
logging.basicConfig(
level=loglevel(args, toml_args),
format=_LOG_FORMAT,
handlers=[
RichHandler(
level=loglevel(args, toml_args),
show_level=False,
show_time=False,
show_path=False,
highlighter=NullHighlighter(),
),
],
)

check_k_version()
Expand Down
9 changes: 5 additions & 4 deletions src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -503,12 +503,13 @@ def create_kcfg_explore() -> KCFGExplore:
redirect_stdout=True,
) as progress:

display_status_bar = not (options.hide_status_bar or options.verbose or options.debug)
failure_infos: list[APRFailureInfo | Exception | None]
if options.workers > 1 and len(tests) > 1:
done_tests = 0
failed_tests = 0
passed_tests = 0
if not options.hide_status_bar:
if display_status_bar:
task = progress.add_task(
f'Multi-proof Mode ({options.workers} workers)',
status='Running',
Expand All @@ -517,7 +518,7 @@ def create_kcfg_explore() -> KCFGExplore:

def update_status_bar(test_id: str, result: Any) -> None:
nonlocal done_tests, failed_tests, passed_tests, progress
if options.hide_status_bar or progress is None:
if not display_status_bar or progress is None:
return
done_tests += 1
proof = foundry.get_apr_proof(test_id)
Expand All @@ -540,14 +541,14 @@ def update_status_bar(test_id: str, result: Any) -> None:

process_pool.close()
process_pool.join()
if not options.hide_status_bar:
if display_status_bar:
if progress is not None:
progress.update(task, status='Finished', advance=1)
failure_infos = [result.get() for result in results]
else:
failure_infos = []
for test in tests:
failure_infos.append(init_and_run_proof(test, None if options.hide_status_bar else progress))
failure_infos.append(init_and_run_proof(test, None if not display_status_bar else progress))

proofs = [foundry.get_apr_proof(test.id) for test in tests]

Expand Down

0 comments on commit 40baed2

Please sign in to comment.