Base class for any error raised by lean-py at the FFI boundary. Attributes: kind: short tag identifying the Lean `IO.Error` constructor (`userError`, `fileNotFound`, `unsupportedOperation`, `invalidArgument`, `permissionDenied`, `interrupted`, `
| 23 | |
| 24 | |
| 25 | class LeanError(RuntimeError): |
| 26 | """Base class for any error raised by lean-py at the FFI boundary. |
| 27 | |
| 28 | Attributes: |
| 29 | kind: short tag identifying the Lean `IO.Error` constructor |
| 30 | (`userError`, `fileNotFound`, `unsupportedOperation`, |
| 31 | `invalidArgument`, `permissionDenied`, `interrupted`, |
| 32 | `noFileOrDirectory`, `inappropriateType`, `unexpected`, |
| 33 | `otherError`, `python`, ...). The set is open-ended; |
| 34 | new Lean toolchains may add ctors. |
| 35 | message: human-readable description. |
| 36 | context: optional dict of extra fields decoded from the ctor |
| 37 | (e.g. `path` for `fileNotFound`). |
| 38 | """ |
| 39 | |
| 40 | __slots__ = ("kind", "message", "context") |
| 41 | |
| 42 | def __init__(self, kind: str, message: str, context: dict | None = None) -> None: |
| 43 | self.kind = kind |
| 44 | self.message = message |
| 45 | self.context = context or {} |
| 46 | # Build a useful str() — RuntimeError uses the first arg. |
| 47 | super().__init__(self._format()) |
| 48 | |
| 49 | def _format(self) -> str: |
| 50 | if self.context: |
| 51 | ctx = ", ".join(f"{k}={v!r}" for k, v in self.context.items()) |
| 52 | return f"[{self.kind}] {self.message} ({ctx})" |
| 53 | return f"[{self.kind}] {self.message}" |
| 54 | |
| 55 | |
| 56 | class LeanPyCallbackError(LeanError): |