Method pickle

lean_py/kernel.py:180–185

Serialise the goal state to disk via Lean's ``saveModuleData``. Round-trips with :meth:`Kernel.goal_unpickle`. Raises on error.

(self, path: str)

    # ---- pickling ----------------------------------------------------------

    def pickle(self, path: str) -> None:
        """Serialise the goal state to disk via Lean's ``saveModuleData``.
        Round-trips with :meth:`Kernel.goal_unpickle`. Raises on error."""
        err = self._kernel._lib.leanpy_kernel_goal_pickle(self._handle, str(path))
        if err:
            raise RuntimeError(f"goal pickle failed: {err}")

    # ---- resume / continue / replay / subsume ------------------------------