Skip to content

Commit

Permalink
Fixing indentation in run_proof_hint (#4589)
Browse files Browse the repository at this point in the history
We missed in the first implementation the indentation that keeps the
temporary file opened. This PR fixed it.

---------

Co-authored-by: Tamás Tóth <[email protected]>
  • Loading branch information
Robertorosmaninho and tothtamas28 authored Aug 14, 2024
1 parent 754fdde commit 9e12e63
Showing 1 changed file with 20 additions and 20 deletions.
40 changes: 20 additions & 20 deletions pyk/src/pyk/ktool/krun.py
Original file line number Diff line number Diff line change
Expand Up @@ -126,27 +126,27 @@ def run_proof_hint(
pgm.write(ntf)
ntf.flush()

args = _build_arg_list(
command='krun',
input_file=Path(ntf.name),
definition_dir=self.definition_dir,
output=output,
parser=parser,
depth=depth,
pmap=pmap,
cmap=cmap,
term=term,
temp_dir=temp_dir,
no_expand_macros=not expand_macros,
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=proof_hint,
)
args = _build_arg_list(
command='krun',
input_file=Path(ntf.name),
definition_dir=self.definition_dir,
output=output,
parser=parser,
depth=depth,
pmap=pmap,
cmap=cmap,
term=term,
temp_dir=temp_dir,
no_expand_macros=not expand_macros,
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=proof_hint,
)

hints_bytes = self.__run_proof_hint_process(
args=args, check=check, pipe_stderr=pipe_stderr, logger=_LOGGER, exec_process=debugger
)
hints_bytes = self.__run_proof_hint_process(
args=args, check=check, pipe_stderr=pipe_stderr, logger=_LOGGER, exec_process=debugger
)

return hints_bytes.stdout

Expand Down

0 comments on commit 9e12e63

Please sign in to comment.