Function test_goal_pickle_round_trip

tests/test_kernel_extra.py:116–132

Pickle a fresh GoalState to disk, reload it, and check that the round-tripped state still has the same shape (one open goal, not solved). The test takes some care to not exercise the GoalState lifecycle issue: it uses cheap field-projecting queries on each state, never the heavy Meta

(kernel)

def test_goal_pickle_round_trip(kernel):
    """Pickle a fresh GoalState to disk, reload it, and check that the
    round-tripped state still has the same shape (one open goal, not
    solved). The test takes some care to not exercise the GoalState
    lifecycle issue: it uses cheap field-projecting queries on each
    state, never the heavy MetaM ops."""
    state = kernel.goal_create("∀ n : Nat, n + 0 = n")
    pre_n_goals = state.n_goals()
    pre_solved = state.is_solved()
    with tempfile.TemporaryDirectory() as d:
        path = os.path.join(d, "goal.olean")
        state.pickle(path)
        assert os.path.getsize(path) > 0
        # Round-trip
        loaded = kernel.goal_unpickle(path)
        assert loaded.n_goals() == pre_n_goals
        assert loaded.is_solved() == pre_solved


# ----------------------------------------------------------------------