From 6d3c88d0036812aa05cdd825e3232f229b567807 Mon Sep 17 00:00:00 2001
From: rexwzh <1073853456@qq.com>
Date: Sat, 21 Dec 2024 05:17:48 +0800
Subject: [PATCH] add three error tests

---
 tests/conftest.py    |  4 ++++
 tests/test_sample.py | 39 ++++++++++++++++++++++++++++++++++++++-
 2 files changed, 42 insertions(+), 1 deletion(-)

diff --git a/tests/conftest.py b/tests/conftest.py
index 5c16597..9c9b667 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -15,6 +15,10 @@
 MINIF2F_TEST_FILE = PROJECT_ROOT / 'experiments/minif2f/test.jsonl'
 MINIF2F_ROOT = PROJECT_ROOT / 'experiments/minif2f/MiniF2F'
 
+@pytest.fixture
+def minif2f_root():
+    return MINIF2F_ROOT
+
 @pytest.fixture
 def minif2f_valid():
     return pd.read_json(MINIF2F_VALID_FILE, lines=True)
diff --git a/tests/test_sample.py b/tests/test_sample.py
index 5edee3b..994127d 100644
--- a/tests/test_sample.py
+++ b/tests/test_sample.py
@@ -4,6 +4,26 @@
 from pantograph.expr import *
 from pantograph.server import TacticFailure
 
+special_cases = [
+"""theorem mathd_numbertheory_552
+  (f g h : ℕ+ → ℕ)
+  (h₀ : ∀ x, f x = 12 * x + 7)
+  (h₁ : ∀ x, g x = 5 * x + 2)
+  (h₂ : ∀ x, h x = Nat.gcd (f x) (g x))
+  (h₃ : Fintype (Set.range h)) :
+  (∑ k in (Set.range h).toFinset, k) = 12 := sorry
+""",
+"""theorem amc12_2000_p15 
+  (f : ℂ → ℂ)
+  (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
+  (h₁ : Fintype (f ⁻¹' {7})) :
+  (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry
+""",
+"""theorem sample (p q r x : ℂ)
+  (h₀ : (x - p) _(x - q) = (r - p)_ (r - q)) :
+  (x - r) _x = (x - r)_ (p + q - r) := sorry
+"""
+]
 
 @pytest.mark.basic
 def test_goal_start_with_ambiguous_type():
@@ -18,4 +38,21 @@ def test_goal_start_with_ambiguous_type():
     state = server.goal_start("1 + 1 = 2")
     with pytest.raises(TacticFailure):
         server.goal_tactic(state, 0, "simp")
-    
+
+@pytest.mark.error
+def test_jsondecode(minif2f_root):
+    server = Server(imports=['Mathlib', 'Init'], project_path=minif2f_root)
+    unit = server.load_sorry(special_cases[0])
+    goal_state, message = unit.goal_state, '\n'.join(unit.messages)
+    assert unit is not None and 'error' not in message.lower() and len(goal_state.goals) == 1
+
+    unit = server.load_sorry(special_cases[1])
+    goal_state, message = unit.goal_state, '\n'.join(unit.messages)
+    assert unit is not None and 'error' not in message.lower() and len(goal_state.goals) == 1
+
+@pytest.mark.error
+def test_proof_with_warn_type(minif2f_root):
+    server = Server(imports=['Mathlib', 'Init'], project_path=minif2f_root)
+    unit = server.load_sorry(special_cases[2])
+    goal_state, message = unit.goal_state, '\n'.join(unit.messages)
+    assert unit is not None and 'error' not in message.lower() and len(goal_state.goals) == 1