From d85cff52645939adb7385cb03431e915b98c1cb4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 18:49:35 -0700 Subject: [PATCH] chore: Library update --- pantograph/server.py | 8 ++++---- src | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/pantograph/server.py b/pantograph/server.py index 28268bc..ddaeeb1 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -22,7 +22,7 @@ class Server: project_path=None, lean_path=None, # Options for executing the REPL. - # Set `{ "automaticMode" : True }` to get a gym-like experience + # Set `{ "automaticMode" : False }` to handle resumption by yourself. options={}, core_options=[], timeout=20, @@ -176,7 +176,7 @@ def get_version(): class TestServer(unittest.TestCase): def test_version(self): - self.assertEqual(get_version(), "0.2.17") + self.assertEqual(get_version(), "0.2.19") def test_expr_type(self): server = Server() @@ -209,7 +209,7 @@ class TestServer(unittest.TestCase): self.assertEqual(len(server.to_remove_goal_states), 0) def test_automatic_mode(self): - server = Server(options={"automaticMode": True}) + 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) @@ -261,7 +261,7 @@ class TestServer(unittest.TestCase): def test_conv_calc(self): - server = Server() + server = Server(options={"automaticMode": False}) state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b") variables = [ diff --git a/src b/src index 9b3eef3..bec84f8 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit 9b3eef35ec40a09bba7140ecfc04dafddbd92c27 +Subproject commit bec84f857bd4f80064213fa5646bef4699191290