Bug/lean multi version

pyproject.toml

@@ -5,7 +5,7 @@ requires = [
 build-backend = "hatchling.build"
 [project]
 name = "itp_interface"
-version = "1.7.0"
+version = "1.8.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]
@@ -41,11 +41,13 @@ dependencies = [
     "urllib3>=2.0.7",
     "mathlibtools==1.3.2",
     "pylspclient==0.0.3",
-    "protobuf==3.20.3; python_version<'3.14'",
-    "grpcio>=1.51.3; python_version<'3.14'"
 ]
 
 [project.optional-dependencies]
+isabelle = [
+    "protobuf==3.20.3; python_version<'3.14'",
+    "grpcio>=1.51.3; python_version<'3.14'",
+]
 app = [
     "streamlit>=1.28.0",
     "scipy>=1.16.0",

src/data/test/lean4_proj/Lean4Proj/Basic.lean

@@ -52,6 +52,10 @@ theorem test3 (p q : Prop) (hp : p) (hq : q)
     exact hq
     exact hp
 
+theorem test_exact (p q : Prop) (hp : p) (hq : q)
+: p ∧ q ∧ p := by
+    exact ⟨hp, hq, hp⟩
+
 theorem imo_1959_p1
   (n : ℕ)
   (h₀ : 0 < n) :

src/itp_interface/lean/simple_lean4_sync_executor.py

@@ -29,7 +29,7 @@
 from itp_interface.tools.iter_helpers import ClonableIterator
 from typing import List, Optional, Tuple, OrderedDict, Dict
 from tempfile import gettempdir, NamedTemporaryFile
-from itp_interface.lean.parsing_helpers import preprocess_declarations
+from itp_interface.lean.parsing_helpers import preprocess_declarations, LeanDeclParser
 
 class SimpleLean4SyncExecutor:
     theorem_regex = r"((((theorem|lemma)[\s]+([^\s:]*))|example)([\S|\s]*?)(:=|=>)[\s]*?)[\s]+"
@@ -687,12 +687,20 @@ def _skip_to_theorem(self, theorem: str):
         theorem_text = thm.text
 
         self._content_till_last_theorem_stmt = "\n".join(self._lines_executed)
-        assert not theorem_text.endswith(':='), "Theorem text should not end with ':='"
-        if SimpleLean4SyncExecutor.ends_with_by_sorry_match.search(theorem_text):
-            # Remove the ':= by sorry' part
-            theorem_text = SimpleLean4SyncExecutor.ends_with_by_sorry_match.sub('', theorem_text).strip() + " :="
+        # On Lean < 4.30.0, the tactic parser returns the full declaration text
+        # (signature + proof) in thm.text with thm.proof=None. On Lean >= 4.30.0
+        # it correctly splits them. Use LeanDeclParser to strip the proof body
+        # from thm.text so we always end up with just the signature + " :=".
+        _parsed = LeanDeclParser(theorem_text).parse()
+        if _parsed.text is not None:
+            theorem_text = _parsed.text.strip() + " :="
         else:
-            theorem_text = theorem_text + " :="
+            assert not theorem_text.endswith(':='), "Theorem text should not end with ':='"
+            if SimpleLean4SyncExecutor.ends_with_by_sorry_match.search(theorem_text):
+                # Remove the ':= by sorry' part
+                theorem_text = SimpleLean4SyncExecutor.ends_with_by_sorry_match.sub('', theorem_text).strip() + " :="
+            else:
+                theorem_text = theorem_text + " :="
         content_until_after_theorem = "\n".join(self._lines_executed) + "\n" + theorem_text
         self._content_till_after_theorem_stmt = content_until_after_theorem.strip()
         assert self._content_till_after_theorem_stmt.endswith(':='), "Content till last theorem statement should not end with ':='"

src/test/simple_env_lean_test.py

@@ -530,6 +530,48 @@ def test_simple_lean4_with_error(self):
                     pretty_print(s1, s2, proof_step, done)
             assert proof_finished, "Proof was not finished"
 
+    def test_simple_lean4_exact_proof(self):
+        """Regression test: theorems whose proof is a single 'exact ...' tactic should
+        produce a valid initial proof state, not 'unexpected token :='."""
+        from itp_interface.rl.proof_state import ProofState
+        from itp_interface.rl.proof_action import ProofAction
+        from itp_interface.rl.simple_proof_env import ProofEnv
+        from itp_interface.tools.proof_exec_callback import ProofExecutorCallback
+        from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy
+        project_folder = "src/data/test/lean4_proj"
+        file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean"
+        helper = LeanHelper()
+        helper.build_lean4_project(project_folder)
+        language = ProofAction.Language.LEAN4
+        # theorem test_exact uses `exact ⟨hp, hq, hp⟩` — a single-tactic proof.
+        # On Lean < 4.30 the tactic parser returned thm.text including the full
+        # proof body, causing '_skip_to_theorem' to append ':=' after the proof
+        # and produce 'unexpected token :='.
+        theorem_name = '{\"namespace\":\"Lean4Proj2\",\"name\":\"test_exact\"}'
+        proof_exec_callback = ProofExecutorCallback(
+            project_folder=project_folder,
+            file_path=file_path,
+            language=language,
+            always_use_retrieval=False,
+            keep_local_context=True
+        )
+        env = ProofEnv(
+            "test_lean4_exact",
+            proof_exec_callback,
+            theorem_name,
+            retrieval_strategy=ProofEnvReRankStrategy.NO_RE_RANK,
+            max_proof_depth=5,
+            always_retrieve_thms=False
+        )
+        with env:
+            state, _, next_state, _, done, info = env.step(ProofAction(
+                ProofAction.ActionType.RUN_TACTIC,
+                language,
+                tactics=['exact ⟨hp, hq, hp⟩']))
+            assert info.error_message is None, \
+                f"Unexpected error on first tactic: {info.error_message}"
+            assert done, "Proof should be complete after 'exact ⟨hp, hq, hp⟩'"
+
     def test_simple_lean4_multiline_multigoal(self):
         from itp_interface.rl.proof_state import ProofState
         from itp_interface.rl.proof_action import ProofAction