Merge pull request #60 from stanford-centaur/version/0.2.25

chore: Update to v0.2.25

README.md

@@ -31,17 +31,7 @@ python3 -m http.server -d .
 
 ## Examples
 
-For API interaction examples, see `examples/README.md`. The examples directory
-also contains a comprehensive Jupyter notebook.
-
-## Experiments
-
-In `experiments/`, there are some experiments:
-1. `minif2f` is an example of executing a `sglang` based prover on the miniF2F dataset
-2. `dsp` is an Lean implementation of Draft-Sketch-Prove
-
-The experiments should be run in `poetry shell`. The environment variable
-`OPENAI_API_KEY` must be set when running experiments calling the OpenAI API.
+For API interaction examples, see `examples/README.md`.
 
 ## Referencing
 

examples/Example/lake-manifest.json

@@ -1,25 +1,25 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/aesop.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
-   "name": "batteries",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop.git",
+   "inputRev": "v4.15.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
-   "name": "aesop",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
-   "inherited": false,
+   "inputRev": "v4.15.0",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Example",
  "lakeDir": ".lake"}

examples/Example/lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop.git" @ "v4.12.0"
+  "https://github.com/leanprover-community/aesop.git" @ "v4.15.0"
 
 package Example
 

examples/sketch.py

@@ -1,9 +1,14 @@
 #!/usr/bin/env python3
 
 from pantograph.server import Server
+from pantograph.expr import TacticDraft
+
+root = """
+theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
+"""
 
 sketch = """
-theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
+by
    -- Consider some n and m in Nats.
    intros n m
    -- Perform induction on n.
@@ -32,5 +37,8 @@
 
 if __name__ == '__main__':
     server = Server()
-    unit, = server.load_sorry(sketch)
+    unit, = server.load_sorry(root)
     print(unit.goal_state)
+
+    sketch = server.goal_tactic(unit.goal_state, 0, TacticDraft(sketch))
+    print(sketch)

pantograph/expr.py

@@ -143,5 +143,11 @@ class TacticExpr:
     Assigns an expression to the current goal
     """
     expr: str
+@dataclass(frozen=True)
+class TacticDraft:
+    """
+    Assigns an expression to the current goal
+    """
+    expr: str
 
-Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr
+Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr | TacticDraft

pantograph/server.py

@@ -17,6 +17,7 @@
     TacticLet,
     TacticCalc,
     TacticExpr,
+    TacticDraft,
 )
 from pantograph.utils import (
     to_sync,
@@ -43,7 +44,9 @@ class ServerError(Exception):
 
 class Server:
     """
-    Main interaction instance with Pantograph
+    Main interaction instance with Pantograph.
+
+    Asynchronous and synchronous versions are provided for each function.
     """
 
     def __init__(self,
@@ -158,7 +161,7 @@ async def restart_async(self):
         self.proc.setecho(False) # Do not send any command before this.
         try:
             ready = await self.proc.readline_async() # Reads the "ready."
-            assert ready.rstrip() == "ready.", f"Server failed to emit ready signal: {ready}; Maybe the project needs to be rebuilt"
+            assert ready.rstrip() == "ready.", f"Server failed to emit ready signal: {ready}; Project Lean version must match Pantograph's Lean version exactly or, it maybe needs to be rebuilt"
         except pexpect.exceptions.TIMEOUT as exc:
             raise RuntimeError("Server failed to emit ready signal in time") from exc
 
@@ -261,10 +264,12 @@ async def goal_tactic_async(self, state: GoalState, goal_id: int, tactic: Tactic
             args["let"] = tactic.branch
             if tactic.binder_name:
                 args["binderName"] = tactic.binder_name
-        elif isinstance(tactic, TacticExpr):
-            args["expr"] = tactic.expr
         elif isinstance(tactic, TacticCalc):
             args["calc"] = tactic.step
+        elif isinstance(tactic, TacticExpr):
+            args["expr"] = tactic.expr
+        elif isinstance(tactic, TacticDraft):
+            args["draft"] = tactic.expr
         else:
             raise RuntimeError(f"Invalid tactic type: {tactic}")
         result = await self.run_async('goal.tactic', args)
@@ -351,6 +356,12 @@ async def load_sorry_async(self, content: str) -> List[CompilationUnit]:
     load_sorry = to_sync(load_sorry_async)
 
     async def env_add_async(self, name: str, t: Expr, v: Expr, is_theorem: bool = True):
+        """
+        Adds a definition to the environment.
+
+        NOTE: May have to accept additional parameters if the definition
+        contains universe mvars.
+        """
         result = await self.run_async('env.add', {
             "name": name,
             "type": t,
@@ -368,6 +379,9 @@ async def env_inspect_async(
             name: str,
             print_value: bool = False,
             print_dependency: bool = False) -> Dict:
+        """
+        Print the type and dependencies of a constant.
+        """
         result = await self.run_async('env.inspect', {
             "name": name,
             "value": print_value,
@@ -379,7 +393,23 @@ async def env_inspect_async(
         return result
     env_inspect = to_sync(env_inspect_async)
 
+    async def env_module_read_async(self, module: str) -> dict:
+        """
+        Reads the content from one Lean module including what constants are in
+        it.
+        """
+        result = await self.run_async('env.module_read', {
+            "module": module
+        })
+        if "error" in result:
+            raise ServerError(result["desc"])
+        return result
+    env_module_read = to_sync(env_module_read_async)
+
     async def env_save_async(self, path: str):
+        """
+        Save the current environment to a file
+        """
         result = await self.run_async('env.save', {
             "path": path,
         })
@@ -388,6 +418,9 @@ async def env_save_async(self, path: str):
     env_save = to_sync(env_save_async)
 
     async def env_load_async(self, path: str):
+        """
+        Load the current environment from a file
+        """
         result = await self.run_async('env.load', {
             "path": path,
         })
@@ -397,6 +430,9 @@ async def env_load_async(self, path: str):
     env_load = to_sync(env_load_async)
 
     async def goal_save_async(self, goal_state: GoalState, path: str):
+        """
+        Save a goal state to a file
+        """
         result = await self.run_async('goal.save', {
             "id": goal_state.state_id,
             "path": path,
@@ -407,6 +443,11 @@ async def goal_save_async(self, goal_state: GoalState, path: str):
     goal_save = to_sync(goal_save_async)
 
     async def goal_load_async(self, path: str) -> GoalState:
+        """
+        Load a goal state from a file.
+
+        User is responsible for keeping track of the environment.
+        """
         result = await self.run_async('goal.load', {
             "path": path,
         })
@@ -424,7 +465,10 @@ async def goal_load_async(self, path: str) -> GoalState:
     goal_load = to_sync(goal_load_async)
 
 
-def get_version():
+def get_version() -> str:
+    """
+    Returns the current Pantograph version for diagnostics purposes.
+    """
     import subprocess
     with subprocess.Popen([_get_proc_path(), "--version"],
                           stdout=subprocess.PIPE,
@@ -435,7 +479,10 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
-        self.assertEqual(get_version(), "0.2.24")
+        """
+        NOTE: Update this after upstream updates.
+        """
+        self.assertEqual(get_version(), "0.2.25")
 
     def test_server_init_del(self):
         import warnings
@@ -612,6 +659,22 @@ def test_load_sorry(self):
         state2 = server.goal_tactic(state1, goal_id=0, tactic="exact h")
         self.assertTrue(state2.is_solved)
 
+        state1b = server.goal_tactic(state0, goal_id=0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry"))
+        self.assertEqual(state1b.goals, [
+            Goal(
+                [Variable(name="p", t="Prop")],
+                target="p ∨ p",
+            ),
+            Goal(
+                [
+                    Variable(name="p", t="Prop"),
+                    Variable(name="h1", t="p ∨ p"),
+                ],
+                target="p → p",
+            ),
+        ])
+
+
     def test_env_add_inspect(self):
         server = Server()
         server.env_add(

pyproject.toml

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "pantograph"
-version = "0.2.24"
+version = "0.2.25"
 description = "A machine-to-machine interaction system for Lean"
 authors = ["Leni Aniva <v@leni.sh>"]
 license = "Apache-2.0"