Skip to content

Commit

Permalink
migrate tests from server.py
Browse files Browse the repository at this point in the history
  • Loading branch information
@RexWzh
RexWzh committed Dec 20, 2024
1 parent 1a607dd commit 2b3f4bf
Show file tree
Hide file tree
Showing 6 changed files with 229 additions and 207 deletions.
198 changes: 0 additions & 198 deletions pantograph/server.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -336,201 +336,3 @@ def get_version():
stdout=subprocess.PIPE,
cwd=_get_proc_cwd()) as p:
return p.communicate()[0].decode('utf-8').strip()


class TestServer(unittest.TestCase):

def test_version(self):
self.assertEqual(get_version(), "0.2.23")

def test_expr_type(self):
server = Server()
t = server.expr_type("forall (n m: Nat), n + m = m + n")
self.assertEqual(t, "Prop")

def test_goal_start(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")
self.assertEqual(state1.state_id, 1)
self.assertEqual(state1.goals, [Goal(
variables=[Variable(name="a", t="Prop")],
target="∀ (q : Prop), a ∨ q → q ∨ a",
name=None,
)])
self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")

del state0
self.assertEqual(len(server.to_remove_goal_states), 1)
server.gc()
self.assertEqual(len(server.to_remove_goal_states), 0)

state0b = server.goal_start("forall (p: Prop), p -> p")
del state0b
self.assertEqual(len(server.to_remove_goal_states), 1)
server.gc()
self.assertEqual(len(server.to_remove_goal_states), 0)

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_have(self):
server = Server()
state0 = server.goal_start("1 + 1 = 2")
state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
self.assertEqual(state1.goals, [
Goal(
variables=[],
target="2 = 1 + 1",
),
Goal(
variables=[Variable(name="h", t="2 = 1 + 1")],
target="1 + 1 = 2",
),
])
def test_let(self):
server = Server()
state0 = server.goal_start("1 + 1 = 2")
state1 = server.goal_tactic(
state0, goal_id=0,
tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
self.assertEqual(state1.goals, [
Goal(
variables=[],
name="h",
target="2 = 1 + 1",
),
Goal(
variables=[Variable(name="h", t="2 = 1 + 1", v="?h")],
target="1 + 1 = 2",
),
])

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 = [
Variable(name="a", t="Nat"),
Variable(name="b", t="Nat"),
Variable(name="h", t="b = 2"),
]
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
self.assertEqual(state2.goals, [
Goal(
variables,
target="1 + a + 1 = a + 1 + 1",
name='calc',
),
Goal(
variables,
target="a + 1 + 1 = a + b",
),
])
state_c1 = server.goal_conv_begin(state2, goal_id=0)
state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
state_c4 = server.goal_conv_end(state_c3)
state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
self.assertTrue(state_c5.is_solved)

state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
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()
unit, = server.load_sorry("example (p: Prop): p → p := sorry")
self.assertIsNotNone(unit.goal_state, f"{unit.messages}")
state0 = unit.goal_state
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)

def test_env_add_inspect(self):
server = Server()
server.env_add(
name="mystery",
t="forall (n: Nat), Nat",
v="fun (n: Nat) => n + 1",
is_theorem=False,
)
inspect_result = server.env_inspect(name="mystery")
self.assertEqual(inspect_result['type'], {'pp': 'Nat → Nat', 'dependentMVars': []})

def test_goal_state_pickling(self):
import tempfile
server = Server()
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
with tempfile.TemporaryDirectory() as td:
path = td + "/goal-state.pickle"
server.goal_save(state0, path)
state0b = server.goal_load(path)
self.assertEqual(state0b.goals, [
Goal(
variables=[
],
target="∀ (p q : Prop), p ∨ q → q ∨ p",
)
])


if __name__ == '__main__':
unittest.main()
1 change: 1 addition & 0 deletions tests/conftest.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
LOGGER_FORMAT = "<green>{level}</green> | <lvl>{message}</lvl>"
logger.add(lambda msg: print(msg, end=''), format=LOGGER_FORMAT, colorize=True)

# Project root
PROJECT_ROOT = Path(__file__).parent.parent

# Experiment for MiniF2F
Expand Down
21 changes: 12 additions & 9 deletions tests/test_minif2f.py
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import pandas as pd
"""Test cases for the minif2f experiment."""

from pandas import DataFrame, Series
from pantograph import Server
from tqdm import tqdm
Expand Down Expand Up @@ -37,9 +38,11 @@ def test_single_case(minif2f_server: Server, minif2f_test: DataFrame):
logger.error(f"Single case test failed with message: {message}")
assert is_valid, f"Failed to load theorem: {message}"

@pytest.mark.basic
@pytest.mark.advance
def test_load_theorem(minif2f_server: Server, minif2f_test: DataFrame, minif2f_valid: DataFrame):
"""Comprehensive test for loading multiple theorems."""
"""Comprehensive test for loading multiple theorems.
use pytest -m "not advance" to skip this test.
"""
logger.info("Theorem loading test")
# Test valid theorems
logger.info("Testing valid theorems...")
Expand Down Expand Up @@ -71,12 +74,12 @@ def test_load_theorem(minif2f_server: Server, minif2f_test: DataFrame, minif2f_v
Test theorems: {total_test - failed_test_count}/{total_test} passed
""")
# Detailed failure report
if failed_valid:
logger.error(f"Failed valid theorems: {failed_valid}")
if failed_test:
logger.error(f"Failed test theorems: {failed_test}")
assert not failed_valid, f"{failed_valid_count} valid theorems failed"
assert not failed_test, f"{failed_test_count} test theorems failed"
if failed_valid or failed_test:
if failed_valid:
err_msg = f"Failed valid theorems: {failed_valid}"
if failed_test:
err_msg += f"\nFailed test theorems: {failed_test}"
raise AssertionError(err_msg)

@pytest.mark.advance
def test_advance_cases():
Expand Down
21 changes: 21 additions & 0 deletions tests/test_sample.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
"""Tests for the special cases."""
import pytest
from pantograph import Server
from pantograph.expr import *
from pantograph.server import TacticFailure


@pytest.mark.basic
def test_goal_start_with_ambiguous_type():
server = Server()
# Valid expression
state = server.goal_start("(1:Nat) + 1 = 2")
assert isinstance(state, GoalState) and len(state.goals) == 1
state2 = server.goal_tactic(state, 0, "rfl")
assert state2.is_solved

# Invalid expression
state = server.goal_start("1 + 1 = 2")
with pytest.raises(TacticFailure):
server.goal_tactic(state, 0, "simp")

Loading

0 comments on commit 2b3f4bf

Please sign in to comment.