From 4e678c7b97f182cc4f157e4ec6ce605da63a4d67 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 5 Jun 2024 14:02:12 -0700
Subject: [PATCH] feat: Use aesop to solve for goals

---
 examples_search/Example/lake-manifest.json | 20 ++++++++--------
 examples_search/Example/lakefile.lean      |  4 ++--
 pantograph/search.py                       |  2 ++
 pantograph/search_llm.py                   | 27 +++++-----------------
 4 files changed, 20 insertions(+), 33 deletions(-)

diff --git a/examples_search/Example/lake-manifest.json b/examples_search/Example/lake-manifest.json
index e1dcad4..260e246 100644
--- a/examples_search/Example/lake-manifest.json
+++ b/examples_search/Example/lake-manifest.json
@@ -10,6 +10,15 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.8.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
@@ -19,15 +28,6 @@
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
@@ -55,7 +55,7 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "rev": "db651742f2c631e5b8525e9aabcf3d61ed094a4a",
diff --git a/examples_search/Example/lakefile.lean b/examples_search/Example/lakefile.lean
index 34d281a..4f468a2 100644
--- a/examples_search/Example/lakefile.lean
+++ b/examples_search/Example/lakefile.lean
@@ -1,8 +1,8 @@
 import Lake
 open Lake DSL
 
--- require aesop from git
---   "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
+require aesop from git
+  "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.8.0-rc1"
diff --git a/pantograph/search.py b/pantograph/search.py
index 26a9b69..ffa6f5c 100644
--- a/pantograph/search.py
+++ b/pantograph/search.py
@@ -73,6 +73,8 @@ class Agent:
             if search_state.is_solved:
                 # if the state is solved, propagate this solved status
                 if search_state.is_root:
+                    if verbose:
+                        print("Search complete: Root state solved")
                     self.reset()
                     return True
 
diff --git a/pantograph/search_llm.py b/pantograph/search_llm.py
index c78eea9..9b50b27 100644
--- a/pantograph/search_llm.py
+++ b/pantograph/search_llm.py
@@ -15,16 +15,11 @@ class LLMAgent(Agent):
         sgl.set_default_backend(sgl.OpenAI("gpt-4"))
 
         self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
-        self.intros = [
-            "intro",
-        ]
         self.tactics = [
-            "simp",
-            "rfl",
-            "decide",
-        ]
-        self.no_space_tactics = [
-            "assumption",
+            "aesop",
+            #"simp",
+            #"rfl",
+            #"decide",
         ]
 
     def next_tactic(self, state: GoalState, goal_id: int, informal_stmt:str="",  informal_proof:str="") -> Optional[Tactic]:
@@ -32,13 +27,7 @@ class LLMAgent(Agent):
         i = self.goal_tactic_id_map[key]
 
         target = state.goals[goal_id].target
-        if target.startswith('∀'):
-            tactics = self.intros
-        elif ' ' in target:
-            tactics = self.tactics
-        else:
-            tactics = self.no_space_tactics
-        if i >= len(tactics):
+        if i >= len(self.tactics):
             new_state = None
             for ii in range(self.n_trials):
                 print(f"===============trail {str(ii)}============")
@@ -51,13 +40,9 @@ class LLMAgent(Agent):
                 if tactic:
                     return tactic
             return None
-    
         else:
             self.goal_tactic_id_map[key] = i + 1
-            return tactics[i]
-
-
-
+            return self.tactics[i]
 
 class TestSearch(unittest.TestCase):