diff --git a/pantograph/expr.py b/pantograph/expr.py index f616354..be648c8 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -93,12 +93,12 @@ class GoalState: @staticmethod def parse_inner(state_id: int, goals: list, _sentinel: list[int]): + assert _sentinel is not None goal_names = { g["name"]: i for i, g in enumerate(goals) } goals = [Goal.parse(g, goal_names) for g in goals] return GoalState(state_id, goals, _sentinel) @staticmethod def parse(payload: dict, _sentinel: list[int]): - assert _sentinel is not None return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel) def __str__(self): diff --git a/pantograph/server.py b/pantograph/server.py index 3e26edd..645897e 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -327,7 +327,7 @@ class Server: }) if "error" in result: raise ServerError(result["desc"]) - return GoalState.parse(result, self.to_remove_goal_states) + return GoalState.parse_inner(state_id, result['goals'], self.to_remove_goal_states) def get_version(): @@ -515,6 +515,22 @@ class TestServer(unittest.TestCase): 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()