From 316358e54ec28e91fe6ab5475097f6e6d1e3d286 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Fri, 23 Aug 2024 13:57:24 -0300
Subject: [PATCH] Introducing `proof hints` feature to be used directly through
 `kevm` binary or poetry. (#14)

Previously, we couldn't parse the `--proof-hints` flag to `krun` through
the poetry/`kevm` binary. As pyk now has support for calling `krun` with
this flag and returning `bytes` as expected, we can now call this new
function `run_proof_hint` and write the bytes to the stdout buffer.
---
 kevm-pyk/src/kevm_pyk/__main__.py | 39 +++++++++++++++++--------------
 1 file changed, 22 insertions(+), 17 deletions(-)

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
index bec3ec9641..733532bf8d 100644
--- a/kevm-pyk/src/kevm_pyk/__main__.py
+++ b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -598,24 +598,29 @@ def exec_run(options: RunOptions) -> None:
         )
 
     if options.proof_hint:
-        kore_input = options.input_file.name.split('.')[0] + '.kore'
-        logging.warning('Proof hints are not supported in the pyk krun at the momment.')
-        logging.info('Saving the input file as %s', kore_input)
-        logging.info(
-            'If you want to emit hints take the krun command shown below and run it replacing the temp file by the kore file generated and append the `--proof-hint` flag to your command.'
+        logging.warning(
+            'Running KEVM with proof hint options enabled, remember to not use this with any `--verbose` mode if you are redirecting its output.'
+        )
+        output_bytes = kevm.run_proof_hint(
+            kore_pattern,
+            depth=options.depth,
+            parser='cat',
+            term=True,
+            expand_macros=options.expand_macros,
+            debugger=options.debugger,
+            proof_hint=True,
+        )
+        sys.stdout.buffer.write(output_bytes)
+    else:
+        kevm.run(
+            kore_pattern,
+            depth=options.depth,
+            term=True,
+            expand_macros=options.expand_macros,
+            output=options.output,
+            check=True,
+            debugger=options.debugger,
         )
-        with open(kore_input, 'w') as f:
-            kore_pattern.write(f)
-
-    kevm.run(
-        kore_pattern,
-        depth=options.depth,
-        term=True,
-        expand_macros=options.expand_macros,
-        output=options.output,
-        check=True,
-        debugger=options.debugger,
-    )
 
 
 def exec_kast(options: KastOptions) -> None: