Added HammerMode

src/itp_interface/tools/coq_executor.py

@@ -13,6 +13,7 @@
 import subprocess
 from itp_interface.coq_ser_api import SerapiInstance, ProofContext, GetCoqAgent, CoqAgent
 from itp_interface.tools.coq_parse_utils import CoqLineByLineReader, CoqStepByStepStdInReader
+from itp_interface.tools.misc_defns import HammerMode
 logger = logging.getLogger()
 
 class CoqExecutor:
@@ -29,7 +30,7 @@ class CoqExecutor:
         "move", "move =>", "move ->", "move => ->", 
         ":", ".", "=>", "{", "}"
     }
-    def __init__(self, project_root: str = None, main_file: str = None, use_hammer: bool = False, timeout_in_sec: int = 60, use_human_readable_proof_context: bool = False, proof_step_iter: typing.Iterator[str] = None, suppress_error_log: bool = False, setup_cmds: typing.List[str] = []):
+    def __init__(self, project_root: str = None, main_file: str = None, use_hammer: typing.Union[bool, HammerMode] = False, timeout_in_sec: int = 60, use_human_readable_proof_context: bool = False, proof_step_iter: typing.Iterator[str] = None, suppress_error_log: bool = False, setup_cmds: typing.List[str] = []):
         assert proof_step_iter is None or isinstance(proof_step_iter, typing.Iterator), \
             "proof_step_iter must be an iterator"
         assert main_file is not None or proof_step_iter is not None, \

src/itp_interface/tools/dynamic_coq_proof_exec.py

@@ -14,6 +14,7 @@
 from itp_interface.tools.coq_parse_utils import CoqLineByLineReader
 from itp_interface.tools.coq_executor import CoqExecutor
 from itp_interface.tools.coq_context_helper import CoqContextHelper
+from itp_interface.tools.misc_defns import HammerMode
 
 class IntertwinedIterator(object):
     def __init__(self, iterator: typing.Optional[typing.Iterator[str]] = None):
@@ -85,7 +86,7 @@ def goal_description_compare(description1: str, descripton2: str) -> int:
             return -1
 
 
-    def __init__(self, coq_context_helper: CoqContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: bool = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, setup_cmds: typing.List[str] = []):
+    def __init__(self, coq_context_helper: CoqContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: typing.Union[bool, HammerMode] = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, setup_cmds: typing.List[str] = []):
         assert proof_file is None or os.path.exists(proof_file), f"Proof file {proof_file} does not exist"
         assert coq_context_helper is not None, "coq_context_helper must not be None"
         self.proof_file = proof_file

src/itp_interface/tools/dynamic_lean4_proof_exec.py

@@ -14,6 +14,7 @@
 from itp_interface.tools.training_data_format import Goal, TrainingDataFormat
 from itp_interface.tools.lean_parse_utils import LeanLineByLineReader
 from itp_interface.tools.lean_context_helper import Lean3ContextHelper
+from itp_interface.tools.misc_defns import HammerMode
 
 class IntertwinedIterator(object):
     def __init__(self, iterator: typing.Optional[typing.Iterator[str]] = None):
@@ -87,7 +88,7 @@ def goal_description_compare(description1: str, descripton2: str) -> int:
             return -1
 
 
-    def __init__(self, coq_context_helper: Lean3ContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: bool = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, keep_local_context = False, enforce_qed: bool = False):
+    def __init__(self, coq_context_helper: Lean3ContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: typing.Union[bool, HammerMode] = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, keep_local_context = False, enforce_qed: bool = False):
         assert proof_file is None or os.path.exists(proof_file), f"Proof file {proof_file} does not exist"
         assert coq_context_helper is not None, "coq_context_helper must not be None"
         self.proof_file = proof_file

src/itp_interface/tools/dynamic_lean_proof_exec.py

@@ -14,6 +14,7 @@
 from itp_interface.tools.training_data_format import Goal, TrainingDataFormat
 from itp_interface.tools.lean_parse_utils import LeanLineByLineReader
 from itp_interface.tools.lean_context_helper import Lean3ContextHelper
+from itp_interface.tools.misc_defns import HammerMode
 
 class IntertwinedIterator(object):
     def __init__(self, iterator: typing.Optional[typing.Iterator[str]] = None):
@@ -87,7 +88,7 @@ def goal_description_compare(description1: str, descripton2: str) -> int:
             return -1
 
 
-    def __init__(self, coq_context_helper: Lean3ContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: bool = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, keep_local_context = False):
+    def __init__(self, coq_context_helper: Lean3ContextHelper, project_folder: str = None, proof_file: str = None, instruction_iter: typing.Optional[str] = None, use_hammer: typing.Union[bool, HammerMode] = False, timeout_in_seconds: int = 60, use_human_readable_proof_context: bool = True, suppress_error_log: bool = True, context_type: ContextType = ContextType.NoContext, keep_local_context = False):
         assert proof_file is None or os.path.exists(proof_file), f"Proof file {proof_file} does not exist"
         assert coq_context_helper is not None, "coq_context_helper must not be None"
         self.proof_file = proof_file

src/itp_interface/tools/isabelle_executor.py

@@ -18,6 +18,7 @@
 from enum import Enum
 from itp_interface.pisa.src.main.python.pisa_client import PisaEnv, initialise_env, IsabelleLemma
 from itp_interface.tools.isabelle_parse_utils import IsabelleLineByLineReader, IsabelleStepByStepStdInReader
+from itp_interface.tools.misc_defns import HammerMode
 logger = logging.getLogger()
 
 class Obligation(typing.NamedTuple):
@@ -79,16 +80,6 @@ def focused_hyps(self) -> typing.List[str]:
         else:
             return []
 
-class HammerMode(Enum):
-    NONE = 'NONE' # Prohibit hammer
-    ALLOW = 'ALLOW' # Allow agent to query hammer
-    AUTO = 'AUTO' # Automatically apply hammer to individual tactics (heuristically)
-    ONESHOT = 'ONESHOT' # Proof attempt in one shot using hammer
-    ALWAYS = 'ALWAYS' # Always use hammer on thesis after a successful proof attempt
-
-    def __str__(self):
-        return self.name
-
 class IsabelleExecutor:
     # This doesn't do the best job of capturing each state changing
     # tactic separately. It relies on the fact the tactics are usually written in an

src/itp_interface/tools/lean4_sync_executor.py

@@ -19,6 +19,7 @@
 from itp_interface.tools.lean_parse_utils import LeanLineByLineReader
 from itp_interface.tools.theorem_details import TheoremDetails
 from itp_interface.lean_server.lean4_repl_interface import ProcessInterface
+from itp_interface.tools.misc_defns import HammerMode
 from typing import Iterator, List, Optional, Tuple, OrderedDict, Generator, Dict
 
 class Lean4SyncExecutor:
@@ -52,7 +53,7 @@ def __init__(self,
         project_root: Optional[str] = None, 
         prefix: Optional[str] = None, 
         main_file: Optional[str] = None, 
-        use_hammer: bool = False, 
+        use_hammer: typing.Union[bool, HammerMode] = False, 
         timeout_in_sec: int = 60, 
         use_human_readable_proof_context: bool = True, 
         proof_step_iter: Optional[Iterator[str]] = None, 

src/itp_interface/tools/lean_cmd_executor.py

@@ -20,6 +20,7 @@
 from itp_interface.lean_server.lean_context import Obligation, ProofContext
 from itp_interface.lean_server.lean_utils import Lean3Utils
 from itp_interface.lean_server.lean3_search_tool import Constants, Lean3Lemma, Lean3SearchTool
+from itp_interface.tools.misc_defns import HammerMode
 logger = logging.getLogger()
 
 class Lean3Executor(object):
@@ -66,7 +67,7 @@ class Lean3Executor(object):
     proof_context_generation_tactic_curlies = "\n}"
     proof_state_running_message = "tactic failed, there are unsolved goals\nstate:"
     search_tools: typing.Dict[str, typing.Any] = {}
-    def __init__(self, project_root: str = None, prefix: str = None, main_file: str = None, use_hammer: bool = False, timeout_in_sec: int = 60, use_human_readable_proof_context: bool = False, proof_step_iter: typing.Iterator[str] = None, suppress_error_log: bool = False, mathlib_root: typing.Optional[str] = None, enable_search: bool = False, namespaces: typing.List[str] = None, keep_local_context: bool = False):
+    def __init__(self, project_root: str = None, prefix: str = None, main_file: str = None, use_hammer: typing.Union[bool, HammerMode] = False, timeout_in_sec: int = 60, use_human_readable_proof_context: bool = False, proof_step_iter: typing.Iterator[str] = None, suppress_error_log: bool = False, mathlib_root: typing.Optional[str] = None, enable_search: bool = False, namespaces: typing.List[str] = None, keep_local_context: bool = False):
         assert proof_step_iter is None or isinstance(proof_step_iter, typing.Iterator), \
             "proof_step_iter must be an iterator"
         assert main_file is not None or proof_step_iter is not None, \

src/itp_interface/tools/misc_defns.py

@@ -0,0 +1,11 @@
+from enum import Enum
+
+class HammerMode(Enum):
+    NONE = 'NONE' # Prohibit hammer
+    ALLOW = 'ALLOW' # Allow agent to query hammer
+    AUTO = 'AUTO' # Automatically apply hammer (heuristically)
+    ONESHOT = 'ONESHOT' # Proof attempt in one shot using hammer
+    ALWAYS = 'ALWAYS' # Always use hammer after a successful proof attempt
+
+    def __str__(self):
+        return self.name

src/itp_interface/tools/proof_exec_callback.py

@@ -20,14 +20,15 @@
 from itp_interface.tools.dynamic_lean_proof_exec import DynamicProofExecutor as DynamicLeanProofExecutor
 from itp_interface.tools.dynamic_lean4_proof_exec import DynamicProofExecutor as DynamicLean4ProofExecutor
 from itp_interface.tools.dynamic_isabelle_proof_exec import DynamicProofExecutor as DynamicIsabelleProofExecutor
+from itp_interface.tools.misc_defns import HammerMode
 
 class ProofExecutorCallback(object):
     def __init__(self,
                 project_folder: str,
                 file_path: str,
                 language: ProofAction.Language = ProofAction.Language.COQ,
                 prefix: str = None,
-                use_hammer: bool = False,
+                use_hammer: typing.Union[bool, HammerMode] = False,
                 timeout_in_secs: int = 60,
                 use_human_readable_proof_context: bool = True,
                 suppress_error_log: bool = True,