Merge pull request #144 from stanford-centaur/build/ci

build: Update build system

Author: lenianiva

.github/workflows/docs.yaml

@@ -33,14 +33,14 @@ jobs:
       run: |
         elan toolchain install $(<src/lean-toolchain)
 
-    - name: Install poetry
+    - name: Install uv
       run: |
-        pip install poetry
-        poetry install --only doc
+        curl -LsSf https://astral.sh/uv/install.sh | sh
+        uv sync
 
     - name: Build documentations
       run: |
-        poetry run jupyter-book build doc
+        uv run --group dev jupyter-book build doc
 
     # Upload the book's HTML as an artifact
     - name: Upload artifact

.github/workflows/test.yaml

@@ -28,11 +28,11 @@ jobs:
       run: |
         elan toolchain install $(<src/lean-toolchain)
 
-    - name: Install poetry
+    - name: Install uv
       run: |
-        pip install poetry
-        poetry install --only doc
+        curl -LsSf https://astral.sh/uv/install.sh | sh
+        uv sync
+
     - name: Run tests
       run: |
-          poetry run python3 -m pantograph.server
-          poetry run python3 -m pantograph.search
+        uv run pytest

README.md

@@ -40,11 +40,19 @@ cd doc/_build/html
 python3 -m http.server -d .
 ```
 
-## Examples
+### Examples
 
 For API interaction examples, see `examples/README.md`.
 
-## Referencing
+### Contributing
+
+Execute unit tests with
+
+```sh
+uv run pytest
+```
+
+## Reference
 
 [Paper Link](https://arxiv.org/abs/2410.16429)
 

pantograph/message.py

@@ -1,7 +1,6 @@
 from dataclasses import dataclass
 from enum import Enum
 from typing import Optional, Self
-import unittest
 
 class Severity(Enum):
     INFORMATION = 1
@@ -72,26 +71,3 @@ class ServerError(Exception):
     """
     Indicates a logical error in the server.
     """
-
-class TestMessage(unittest.TestCase):
-
-    def test_severity(self):
-        self.assertEqual(str(Severity.ERROR), "error")
-    def test_message(self):
-        m = Message(
-            data="hi",
-            pos=Position(12, 34),
-            pos_end=Position(56, 78),
-            severity=Severity.WARNING,
-        )
-        self.assertEqual(str(m), "12:34-56:78: warning: hi")
-
-        m = Message(
-            data="hi",
-            pos=Position(0, 0),
-            severity=Severity.ERROR,
-        )
-        self.assertEqual(str(m), "0:0: error: hi")
-
-if __name__ == '__main__':
-    unittest.main()

pantograph/search.py

@@ -1,12 +1,14 @@
+from .server import Server, TacticFailure, ServerError
+from .expr import Expr, Tactic, GoalState, Site
+
 import random
 from abc import abstractmethod
 import time
 from dataclasses import dataclass
 from typing import Optional, List
-import collections, unittest
+import collections
 from math import log, sqrt
-from pantograph.server import Server, TacticFailure, ServerError
-from pantograph.expr import Expr, Tactic, GoalState, Site
+
 
 
 @dataclass
@@ -446,55 +448,3 @@ def next_tactic(
         return tactics[i]
 
 
-class TestSearch(unittest.TestCase):
-
-    def test_solve(self):
-
-        server = Server()
-        agent = DumbAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), p -> p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
-        self.assertTrue(flag)
-    def test_solve_big(self):
-
-        server = Server()
-        agent = DumbAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        self.assertTrue(flag)
-
-class TestMCTSSearch(unittest.TestCase):
-
-    def test_solve(self):
-
-        server = Server()
-        agent = DumbMCTSAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), p -> p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
-        self.assertTrue(flag)
-    def test_solve_big(self):
-
-        server = Server()
-        agent = DumbMCTSAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            max_steps=200,
-            verbose=False)
-        self.assertTrue(flag)
-
-
-if __name__ == '__main__':
-    unittest.main()