Parse a Lean `IO.userError` string produced by `raise_py_error`. The C bridge formats Python errors as `" : "`. If `raw` matches that shape, return `(typeName, message)`. Otherwise return `("", raw)` and let the caller wrap it as a generic LeanError.
(raw: str)
| 78 | |
| 79 | |
| 80 | def parse_io_error_message(raw: str) -> tuple[str, str]: |
| 81 | """Parse a Lean `IO.userError` string produced by `raise_py_error`. |
| 82 | |
| 83 | The C bridge formats Python errors as `"<TypeName>: <message>"`. If |
| 84 | `raw` matches that shape, return `(typeName, message)`. Otherwise |
| 85 | return `("", raw)` and let the caller wrap it as a generic LeanError. |
| 86 | """ |
| 87 | if not raw: |
| 88 | return "", "" |
| 89 | sep = raw.find(": ") |
| 90 | if sep <= 0: |
| 91 | return "", raw |
| 92 | typename = raw[:sep] |
| 93 | # Heuristic: Python exception type names are CamelCase identifiers, |
| 94 | # no whitespace. Anything else is probably not a Python error. |
| 95 | if not typename.replace("_", "").isalnum() or not typename: |
| 96 | return "", raw |
| 97 | if not typename[0].isupper(): |
| 98 | return "", raw |
| 99 | return typename, raw[sep + 2 :] |
| 100 | |
| 101 | |
| 102 | __all__ = [ |