From 39d908d3e8a6229d0b06d32391625092927d157a Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 3 Mar 2025 18:30:46 -0600 Subject: [PATCH] Added HammerMode --- src/itp_interface/tools/coq_executor.py | 3 ++- src/itp_interface/tools/dynamic_coq_proof_exec.py | 3 ++- src/itp_interface/tools/dynamic_lean4_proof_exec.py | 3 ++- src/itp_interface/tools/dynamic_lean_proof_exec.py | 3 ++- src/itp_interface/tools/isabelle_executor.py | 11 +---------- src/itp_interface/tools/lean4_sync_executor.py | 3 ++- src/itp_interface/tools/lean_cmd_executor.py | 3 ++- src/itp_interface/tools/misc_defns.py | 11 +++++++++++ src/itp_interface/tools/proof_exec_callback.py | 3 ++- 9 files changed, 26 insertions(+), 17 deletions(-) create mode 100644 src/itp_interface/tools/misc_defns.py diff --git a/src/itp_interface/tools/coq_executor.py b/src/itp_interface/tools/coq_executor.py index f464397..30d077a 100644 --- a/src/itp_interface/tools/coq_executor.py +++ b/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, \ diff --git a/src/itp_interface/tools/dynamic_coq_proof_exec.py b/src/itp_interface/tools/dynamic_coq_proof_exec.py index 4e5dd32..9e0814e 100644 --- a/src/itp_interface/tools/dynamic_coq_proof_exec.py +++ b/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 diff --git a/src/itp_interface/tools/dynamic_lean4_proof_exec.py b/src/itp_interface/tools/dynamic_lean4_proof_exec.py index 5716915..bb365b2 100644 --- a/src/itp_interface/tools/dynamic_lean4_proof_exec.py +++ b/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 diff --git a/src/itp_interface/tools/dynamic_lean_proof_exec.py b/src/itp_interface/tools/dynamic_lean_proof_exec.py index 75733b0..c27f484 100644 --- a/src/itp_interface/tools/dynamic_lean_proof_exec.py +++ b/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 diff --git a/src/itp_interface/tools/isabelle_executor.py b/src/itp_interface/tools/isabelle_executor.py index 95999c7..289a890 100644 --- a/src/itp_interface/tools/isabelle_executor.py +++ b/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 diff --git a/src/itp_interface/tools/lean4_sync_executor.py b/src/itp_interface/tools/lean4_sync_executor.py index 86a00f2..22b18ba 100644 --- a/src/itp_interface/tools/lean4_sync_executor.py +++ b/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, diff --git a/src/itp_interface/tools/lean_cmd_executor.py b/src/itp_interface/tools/lean_cmd_executor.py index 39d7a96..c62ba72 100644 --- a/src/itp_interface/tools/lean_cmd_executor.py +++ b/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, \ diff --git a/src/itp_interface/tools/misc_defns.py b/src/itp_interface/tools/misc_defns.py new file mode 100644 index 0000000..b4a7d64 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/itp_interface/tools/proof_exec_callback.py b/src/itp_interface/tools/proof_exec_callback.py index d029dcb..0494c1e 100644 --- a/src/itp_interface/tools/proof_exec_callback.py +++ b/src/itp_interface/tools/proof_exec_callback.py @@ -20,6 +20,7 @@ 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, @@ -27,7 +28,7 @@ def __init__(self, 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,