Dev (#2)

* add pytest dependency

* add test code for minif2f

* update minif2f from purewhite

* add github action

* migrate tests from server.py

* add three error tests

* fix minif2f statements

* add pytest marks

* minif2f: fix & check

* update tests

* ignore poetry.lock

* fix json dumps in server.py

* add pylock

Author: RexWzh

.github/workflows/test.yaml

@@ -0,0 +1,59 @@
+name: Python Package
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        python-version: ["3.10"]
+        os: [ubuntu-latest]
+            
+    steps:
+    - name: Install elan
+      run: |
+        set -o pipefail
+        curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      
+    - uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: Install Dependencies
+      run: |
+        pushd experiments/minif2f/MiniF2F/
+        lake exe cache get && lake build
+        popd
+    - name: Cache dependencies
+      uses: actions/cache@v3
+      with:
+        path: |
+          ~/.cache/pip
+          ~/.cache/pypoetry
+        key: ${{ runner.os }}-poetry-${{ hashFiles('**/poetry.lock') }}
+        restore-keys: |
+          ${{ runner.os }}-poetry-
+          
+    - name: Install Poetry
+      run: |
+        curl -sSL https://install.python-poetry.org | python3 -
+        echo "export PATH=$HOME/.local/bin:$PATH" >> $GITHUB_ENV
+    - name: Set up Python ${{ matrix.python-version }}
+      uses: actions/setup-python@v2
+      with:
+        python-version: ${{ matrix.python-version }}
+    - name: Install dependencies
+      run: |
+        poetry build
+        poetry install
+    - name: Test with pytest
+      run: |
+        poetry run pytest -s tests/

.gitignore

@@ -8,4 +8,4 @@
 
 # Output
 /dist
-/venv
+/venv

build.py custom_build.pybuild.py renamed to custom_build.py

@@ -125,7 +125,7 @@ def run(self, cmd, payload):
         :meta private:
         """
         assert self.proc
-        s = json.dumps(payload)
+        s = json.dumps(payload, ensure_ascii=False)
         self.proc.sendline(f"{cmd} {s}")
         try:
             line = self.proc.readline()
@@ -339,201 +339,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.24")
-
-    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()