repl: add LeanError/TacticError exception hierarchy - #2
Merged
Merged
Conversation
All failures raised bare RuntimeError, forcing callers (RL / proof search loops) to string-match messages to tell an expected tactic failure from a parse error, unknown state, or internal error. - LeanError(RuntimeError): base for leotower Lean-operation errors, raised by set_goal / check / inspect / run_cmd failures. - TacticError(LeanError): tactic parse/elaboration/application failure; session and replay state stay usable. Raised by run_tac / run_tacs (try_run_tac / try_run_tacs are non-raising and untouched). - Repl wrappers re-raise via 'raise NewType(str(e)) from e', preserving the original message and cause. - Backward compatible: both refine RuntimeError, so existing 'except RuntimeError' handlers keep working (covered by tests). Rust unchanged; existing error tests (match="...") pass as-is.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
W-403：在 Python 包装层引入可区分、可捕获的异常层级（向后兼容）。
LeanError(RuntimeError)/TacticError(LeanError)，加入__all__Repl包装层按类型重抛（raise NewType(str(e)) from e，保留消息与 cause）：run_tac/run_tacs→TacticError；set_goal/check/inspect/run_cmd→LeanErrorexcept RuntimeError捕获逻辑不受影响（有测试覆盖）uv run pytest63 passed / 1 skipped评审：Leo3 Reviewer 已通过（W-403 评论线程）。