aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

Merge branch 'frontend/collect-holes' into search

This commit is contained in:
Leni Aniva 2024-09-13 17:14:20 -07:00
parent 27599f7fad 2f70e6d918
commit 6f4c26ecee
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
18 changed files with 2748 additions and 243 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@ -8,6 +8,3 @@
# Output
/dist
/venv
pantograph/pantograph
pantograph/lean-toolchain

14
README.md
View File

@ -22,3 +22,17 @@ python -m pantograph.server
```
The tests in `pantograph/server.py` also serve as simple interaction examples
## Examples
See `examples/README.md`
## Referencing
```bib
@misc{pantograph,
title = "Pantograph, A Machine-to-Machine Interface for Lean 4",
author = {Aniva, Leni and Miranda, Brando and Sun, Chuyue},
year = 2024,
howpublished = {\url{https://github.com/lenianiva/PyPantograph}}
}
```

6
build.py
View File

@ -6,10 +6,10 @@ from pathlib import Path
PATH_PANTOGRAPH = Path("./src")
PATH_PY = Path("./pantograph")
with subprocess.Popen(["make"], cwd=PATH_PANTOGRAPH) as p:
with subprocess.Popen(["lake", "build", "repl"], cwd=PATH_PANTOGRAPH) as p:
p.wait()
path_executable = PATH_PY / "pantograph"
shutil.copyfile(PATH_PANTOGRAPH / ".lake/build/bin/pantograph", path_executable)
path_executable = PATH_PY / "pantograph-repl"
shutil.copyfile(PATH_PANTOGRAPH / ".lake/build/bin/repl", path_executable)
os.chmod(path_executable, os.stat(path_executable).st_mode | stat.S_IEXEC)
shutil.copyfile(PATH_PANTOGRAPH / "lean-toolchain", PATH_PY / "lean-toolchain")

3
examples/Example/Example.lean
View File

@ -1,11 +1,12 @@
import Aesop
-- Ensure that Aesop is running
/-- Ensure that Aesop is running -/
example : α → α :=
by aesop
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
intro p q h
-- Here are some comments
cases h
. apply Or.inr
assumption

16
examples/Example/lake-manifest.json
View File

@ -1,11 +1,12 @@
{"version": 7,
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover/std4",
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "3025cb124492b423070f20cf0a70636f757d117f",
"name": "std",
"scope": "",
"rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
@ -13,11 +14,12 @@
{"url": "https://github.com/leanprover-community/aesop.git",
"type": "git",
"subDir": null,
"rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
"scope": "",
"rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.8.0-rc1",
"inputRev": "v4.10.0-rc1",
"inherited": false,
"configFile": "lakefile.lean"}],
"configFile": "lakefile.toml"}],
"name": "Example",
"lakeDir": ".lake"}

2
examples/Example/lakefile.lean
View File

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

2
examples/Example/lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:v4.8.0-rc1
leanprover/lean4:v4.10.0-rc1

17
examples/README.md
View File

@ -1,4 +1,11 @@
# Usage Example
# Examples
For a quick introduction of the API, fire up Jupyter and open `all.ipynb`. (Did
you remember to `poetry install`?)
``` sh
poetry run jupyter notebook
```
This example showcases how to bind library dependencies and execute the `Aesop`
tactic in Lean. First build the example project:
@ -7,9 +14,15 @@ pushd Example
lake build
popd
```
This would generate compiled `.olean` files. Then run the example from the
This would generate compiled `.olean` files. Then run one of the examples from the
project root:
``` sh
poetry run examples/aesop.py
poetry run examples/data.py
```
Warning: If you make modifications to any Lean files, you must re-run `lake
build`! Moreover, the version of the Lean used in the example folder (including
dependencies in `lakefile.lean` and `lean-toolchain`) **must match exactly**
with the version in `src/`!

453
examples/all.ipynb Normal file
View File

@ -0,0 +1,453 @@
{
"cells": [
{
"cell_type": "markdown",
"id": "a1078f98-fcaf-4cda-8ad4-3cbab44f114b",
"metadata": {},
"source": [
"# Pantograph Example\n",
"\n",
"The only interface for interacting with Pantograph is the `Server` class. It can be used either standalone (with no Lean project specified) or in a Lean project in order to access the project's symbols (e.g. Mathlib).\n",
"\n",
"The server's `imports` argument must be specified as a list of Lean modules to import. With no import statements, there are no symbols available and no useful work can be done. By default, `imports` is `[\"Init\"]`."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
"metadata": {},
"outputs": [],
"source": [
"from pantograph import Server\n",
"\n",
"server = Server()"
]
},
{
"cell_type": "markdown",
"id": "1fbdb837-740e-44ef-a7e9-c40f79584639",
"metadata": {},
"source": [
"We can initialize a proof by providing the target statement."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
"metadata": {},
"outputs": [],
"source": [
"state0 = server.goal_start(\"forall (p : Prop), p -> p\")"
]
},
{
"cell_type": "markdown",
"id": "deb7994a-273f-4b52-be2d-e1086d4c1d55",
"metadata": {},
"source": [
"This invocation creates a *goal state*, which consists of a finite number of goals. "
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"state0"
]
},
{
"cell_type": "markdown",
"id": "274f50da-85c1-445e-bf9f-cb716f66e36f",
"metadata": {},
"source": [
"Execute tactics on the goal state via `Server.goal_tactic`:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[])"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
"state1"
]
},
{
"cell_type": "markdown",
"id": "1c1c5ab4-5518-40b0-8a2f-50e095a3702a",
"metadata": {},
"source": [
"Recover the usual string form of a goal by the `str` function:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'p✝ : Prop\\n⊢ p✝ → p✝'"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"str(state1.goals[0])"
]
},
{
"cell_type": "markdown",
"id": "fc560b88-0222-4e40-bff9-37ab70af075e",
"metadata": {},
"source": [
"When a tactic fails, it throws an exception:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[\"tactic 'assumption' failed\\np✝ : Prop\\n⊢ p✝ → p✝\"]\n"
]
}
],
"source": [
"try:\n",
" state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
" print(\"Should not reach this\")\n",
"except Exception as e:\n",
" print(e)"
]
},
{
"cell_type": "markdown",
"id": "c801bbb4-9248-4f75-945b-1dd665bb08d1",
"metadata": {},
"source": [
"A state with no goals is considered solved"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"GoalState(state_id=3, goals=[], _sentinel=[])"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
"state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
"state3"
]
},
{
"cell_type": "markdown",
"id": "aa5a2800-cae3-48df-b746-d19a8d84eaf5",
"metadata": {},
"source": [
"Execute `Server.gc()` to clean up unused goals once in a while"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
"metadata": {},
"outputs": [],
"source": [
"server.gc()"
]
},
{
"cell_type": "markdown",
"id": "78cfb9ac-c5ec-4901-97a5-4d19e6b8ecbb",
"metadata": {},
"source": [
"## Loading Projects\n",
"\n",
"Pantograph would not be useful if it could not load symbols from other projects. In `examples/Example` is a standard Lean 4 project, with its toolchain version precisely equal to the toolchain version of Pantograph. Executing `lake new PROJECT_NAME` or `lake init` in an empty folder initializes a project according to this specification. To use a project in Pantograph, compile the project by running `lake build` in its root directory. This sets up output folders and builds the binary Lean files.\n",
"\n",
"Load the example project by providing `project_path` and `lean_path` to `Server`:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
"$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean\\n'\n"
]
}
],
"source": [
"import subprocess, os\n",
"from pathlib import Path\n",
"def get_project_and_lean_path():\n",
" cwd = Path(os.getcwd()).resolve() / 'Example'\n",
" p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)\n",
" return cwd, p\n",
"project_path, lean_path = get_project_and_lean_path()\n",
"print(f\"$PWD: {project_path}\")\n",
"print(f\"$LEAN_PATH: {lean_path}\")\n",
"server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)"
]
},
{
"cell_type": "markdown",
"id": "67123741-3d23-4077-98ab-91110b4e39f1",
"metadata": {},
"source": [
"With the project loaded, all dependencies of the project, be it Mathlib or Aesop, are now available."
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")\n",
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"aesop\")\n",
"state1.is_solved"
]
},
{
"cell_type": "markdown",
"id": "8c3f9d90-bacc-4cba-95a4-23cc31a58a4f",
"metadata": {},
"source": [
"## Reading Symbols\n",
"\n",
"Pantograph can also query proof states from a project by directly calling into Lean's compiler internals. Run the Lean compiler on a Lean file via `Server.tactic_invocations`. Feeding in the absolute path is preferred."
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"==== #0 ====\n",
"/-- Ensure that Aesop is running -/\n",
"example : α → α :=\n",
" by aesop\n",
"\n",
"\n",
"==== #1 ====\n",
"example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
" intro p q h\n",
" -- Here are some comments\n",
" cases h\n",
" . apply Or.inr\n",
" assumption\n",
" . apply Or.inl\n",
" assumption\n",
"\n",
"==== Invocations ====\n",
"α : Sort ?u.7\n",
"⊢ α → α\n",
"aesop\n",
"\n",
"\n",
"⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
"intro p q h\n",
"p q : Prop\n",
"h : p ∨ q\n",
"⊢ q ∨ p\n",
"\n",
"p q : Prop\n",
"h : p ∨ q\n",
"⊢ q ∨ p\n",
"cases h\n",
"case inl\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ q ∨ p\n",
"case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
"\n",
"case inl\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ q ∨ p\n",
"apply Or.inr\n",
"case inl.h\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ p\n",
"\n",
"case inl.h\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ p\n",
"assumption\n",
"\n",
"\n",
"case inr\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q ∨ p\n",
"apply Or.inl\n",
"case inr.h\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q\n",
"\n",
"case inr.h\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q\n",
"assumption\n",
"\n",
"\n"
]
}
],
"source": [
"units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
"for i, u in enumerate(units):\n",
" print(f\"==== #{i} ====\")\n",
" print(u)\n",
"print(\"==== Invocations ====\")\n",
"for i in invocations:\n",
" print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
]
},
{
"cell_type": "markdown",
"id": "8762b719-d13b-4714-84ff-48c44b18f364",
"metadata": {},
"source": [
"### Loading a theorem for the agent to prove\n",
"\n",
"For this to work, write `sorry` in the place where you would like your agent to do work, for example\n",
"```lean\n",
"example : (p q: Prop): Or p q -> Or q p := sorry\n",
"```\n",
"Then use the `Server.load_sorry`. As long as you only have one statement in `command`, it will give you exactly one goal state. A command with no `sorry`s results in no goal states.\n",
"\n",
"Note: Since a syntactically incorrect command will not generate `sorry`s, they will be sliently ignored by the frontend. Check if this is the case if the function returns no goals."
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "3c515d2b-6910-499e-953b-bc69dc0e0a57",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p'), Variable(t='Prop', v=None, name='q')], target='p ∨ q → q ∨ p', name=None, is_conversion=False)], _sentinel=[0])\n"
]
}
],
"source": [
"state0, = server.load_sorry(\"example (p q: Prop): Or p q -> Or q p := sorry\")\n",
"print(state0)"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "50b90547-fcbf-419f-866e-a6ebcc925c5f",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.4"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

10
examples/compile-tactics.py → examples/data.py
View File

@ -14,6 +14,10 @@ if __name__ == '__main__':
print(f"$PWD: {project_path}")
print(f"$LEAN_PATH: {lean_path}")
server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
data = server.compile_tactics("Example")
for (before, tactic, after) in data:
print(f"{before}\n{tactic}\n{after}\n\n")
units, invocations = server.tactic_invocations(project_path / "Example.lean")
for i, u in enumerate(units):
print(f"==== #{i} ====")
print(u)
print("==== Invocations ====")
for i in invocations:
print(f"{i.before}\n{i.tactic}\n{i.after}\n")

2
pantograph/.gitignore vendored Normal file
View File

@ -0,0 +1,2 @@
pantograph-repl
lean-toolchain

1
pantograph/__init__.py
View File

@ -0,0 +1 @@
from pantograph.server import Server

13
pantograph/compiler.py Normal file
View File

@ -0,0 +1,13 @@
from dataclasses import dataclass
@dataclass(frozen=True)
class TacticInvocation:
before: str
after: str
tactic: str
@staticmethod
def parse(payload: dict):
return TacticInvocation(before=payload["goalBefore"],
after=payload["goalAfter"],
tactic=payload["tactic"])

10
pantograph/expr.py
View File

@ -78,11 +78,13 @@ class GoalState:
return not self.goals
@staticmethod
def parse(payload: dict, _sentinel: list[int]):
state_id = payload["nextStateId"]
goal_names = { g["name"]: i for i,g in enumerate(payload["goals"]) }
goals = [Goal.parse(g, goal_names) for g in payload["goals"]]
def parse_inner(state_id: int, goals: list, _sentinel: list[int]):
goal_names = { g["name"]: i for i, g in enumerate(goals) }
goals = [Goal.parse(g, goal_names) for g in goals]
return GoalState(state_id, goals, _sentinel)
@staticmethod
def parse(payload: dict, _sentinel: list[int]):
return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
def __str__(self):
return "\n".join([str(g) for g in self.goals])

133
pantograph/server.py
View File

@ -2,14 +2,17 @@
Class which manages a Pantograph instance. All calls to the kernel uses this
interface.
"""
import json, pexpect, pathlib, unittest, os
import json, pexpect, unittest, os
from typing import Union
from pathlib import Path
from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
Tactic, TacticHave, TacticCalc
from pantograph.compiler import TacticInvocation
def _get_proc_cwd():
return pathlib.Path(__file__).parent
return Path(__file__).parent
def _get_proc_path():
return _get_proc_cwd() / "pantograph"
return _get_proc_cwd() / "pantograph-repl"
class TacticFailure(Exception):
pass
@ -22,7 +25,10 @@ class Server:
imports=["Init"],
project_path=None,
lean_path=None,
options=[],
# Options for executing the REPL.
# Set `{ "automaticMode" : False }` to handle resumption by yourself.
options={},
core_options=[],
timeout=20,
maxread=1000000):
"""
@ -37,7 +43,8 @@ class Server:
self.proc_path = _get_proc_path()
self.options = options
self.args = " ".join(imports + [f'--{opt}' for opt in options])
self.core_options = core_options
self.args = " ".join(imports + [f'--{opt}' for opt in core_options])
self.proc = None
self.restart()
@ -55,10 +62,16 @@ class Server:
f"{self.proc_path} {self.args}",
encoding="utf-8",
maxread=self.maxread,
timeout=self.timeout,
cwd=self.project_path,
env=env,
)
self.proc.setecho(False)
self.proc.setecho(False) # Do not send any command before this.
ready = self.proc.readline() # Reads the "ready."
assert ready == "ready.\r\n", f"Server failed to emit ready signal: {ready}; Maybe the project needs to be rebuilt"
if self.options:
self.run("options.set", self.options)
self.run('options.set', {'printDependentMVars': True})
@ -69,9 +82,8 @@ class Server:
s = json.dumps(payload)
self.proc.sendline(f"{cmd} {s}")
try:
self.proc.expect("{.*}\r\n", timeout=self.timeout)
output = self.proc.match.group()
return json.loads(output)
line = self.proc.readline()
return json.loads(line)
except pexpect.exceptions.TIMEOUT as exc:
raise exc
@ -141,12 +153,38 @@ class Server:
raise ServerError(result["parseError"])
return GoalState.parse(result, self.to_remove_goal_states)
def compile_tactics(self, module: str) -> list[tuple[str, str, str]]:
result = self.run('compile.tactics', {'module': module})
def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], list[TacticInvocation]]:
"""
Collect tactic invocation points in file, and return them.
"""
result = self.run('frontend.process', {
'fileName': str(file_name),
'invocations': True,
"sorrys": False,
})
if "error" in result:
raise ServerError(result["desc"])
return [(i['goalBefore'], i['tactic'], i['goalAfter']) for i in result['invocations']]
with open(file_name, 'rb') as f:
content = f.read()
units = [content[begin:end].decode('utf-8') for begin,end in result['units']]
invocations = [TacticInvocation.parse(i) for i in result['invocations']]
return units, invocations
def load_sorry(self, command: str) -> list[GoalState]:
result = self.run('frontend.process', {
'file': command,
'invocations': False,
"sorrys": True,
})
if "error" in result:
raise ServerError(result["desc"])
states = [
GoalState.parse_inner(state_id, goals, self.to_remove_goal_states)
for (state_id, goals) in result['goalStates']
]
return states
@ -161,7 +199,7 @@ def get_version():
class TestServer(unittest.TestCase):
def test_version(self):
self.assertEqual(get_version(), "0.2.15")
self.assertEqual(get_version(), "0.2.19")
def test_expr_type(self):
server = Server()
@ -193,8 +231,60 @@ class TestServer(unittest.TestCase):
server.gc()
self.assertEqual(len(server.to_remove_goal_states), 0)
def test_conv_calc(self):
def test_automatic_mode(self):
server = Server()
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
self.assertEqual(len(server.to_remove_goal_states), 0)
self.assertEqual(state0.state_id, 0)
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
self.assertEqual(state1.state_id, 1)
self.assertEqual(state1.goals, [Goal(
variables=[
Variable(name="a", t="Prop"),
Variable(name="b", t="Prop"),
Variable(name="h", t="a ∨ b"),
],
target="b ∨ a",
name=None,
)])
state2 = server.goal_tactic(state1, goal_id=0, tactic="cases h")
self.assertEqual(state2.goals, [
Goal(
variables=[
Variable(name="a", t="Prop"),
Variable(name="b", t="Prop"),
Variable(name="h✝", t="a"),
],
target="b ∨ a",
name="inl",
),
Goal(
variables=[
Variable(name="a", t="Prop"),
Variable(name="b", t="Prop"),
Variable(name="h✝", t="b"),
],
target="b ∨ a",
name="inr",
),
])
state3 = server.goal_tactic(state2, goal_id=1, tactic="apply Or.inl")
state4 = server.goal_tactic(state3, goal_id=0, tactic="assumption")
self.assertEqual(state4.goals, [
Goal(
variables=[
Variable(name="a", t="Prop"),
Variable(name="b", t="Prop"),
Variable(name="h✝", t="a"),
],
target="b ∨ a",
name="inl",
)
])
def test_conv_calc(self):
server = Server(options={"automaticMode": False})
state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
variables = [
@ -226,6 +316,19 @@ class TestServer(unittest.TestCase):
state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
self.assertTrue(state4.is_solved)
def test_load_sorry(self):
server = Server()
state0, = server.load_sorry("example (p: Prop): p → p := sorry")
self.assertEqual(state0.goals, [
Goal(
[Variable(name="p", t="Prop")],
target="p → p",
),
])
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro h")
state2 = server.goal_tactic(state1, goal_id=0, tactic="exact h")
self.assertTrue(state2.is_solved)
if __name__ == '__main__':
unittest.main()

2301
poetry.lock generated
View File

File diff suppressed because it is too large Load Diff

3
pyproject.toml
View File

@ -18,6 +18,9 @@ tiktoken = "^0.7.0"
generate-setup-file = false
script = "build.py"
[tool.poetry.group.dev.dependencies]
notebook = "^7.2.1"
[build-system]
requires = ["poetry-core"]
build-backend = "poetry.core.masonry.api"

2
src

@ -1 +1 @@
Subproject commit b9b16ba0e9d99279837527bcb40176277d11e725
Subproject commit bec84f857bd4f80064213fa5646bef4699191290