diff --git a/README.md b/README.md index 6c290c7..5485820 100644 --- a/README.md +++ b/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 diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json index fe0adeb..1792824 100644 --- a/examples/Example/lake-manifest.json +++ b/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"} diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean index a85cd79..40f8e92 100644 --- a/examples/Example/lakefile.lean +++ b/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 diff --git a/examples/sketch.py b/examples/sketch.py index f8cad14..8ba19fc 100644 --- a/examples/sketch.py +++ b/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) diff --git a/pantograph/expr.py b/pantograph/expr.py index be648c8..5ad1a33 100644 --- a/pantograph/expr.py +++ b/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 diff --git a/pantograph/server.py b/pantograph/server.py index 5f8278c..0853049 100644 --- a/pantograph/server.py +++ b/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( diff --git a/pyproject.toml b/pyproject.toml index 6a90700..06d7d99 100644 --- a/pyproject.toml +++ b/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 "] license = "Apache-2.0" diff --git a/src b/src index ef4e5ec..4435a64 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit ef4e5ecbf8057c6baf542391d4c40ec068810aa4 +Subproject commit 4435a6459cddc0661d39d2f370887eff007c94fd