Default recover_from_error to false for most commands #1448
Conversation
| @@ -1,6 +1,6 @@ | |||
| type_error_at_eval_expr.lean:3:0: error: eval_expr failed due to type error | |||
| nested exception message: | |||
| type mismatch at definition '_eval_expr.16.423', has type | |||
| type mismatch at definition '_eval_expr.16.436', has type | |||
| list ℕ | |||
| but is expected to have type | |||
| ℕ | |||
There was a problem hiding this comment.
@leodemoura Should we just replace integral name parts with _ or something by default? Of course, ideally users should never see private names at all (by default).
There was a problem hiding this comment.
I think this is a good idea. BTW, we should have an option for disabling this kind of cleanup. The option is mostly for ourselves when debugging crazy bugs.
|
It can be argued whether commands such as |
…or most commands Fixes leanprover#1446
uncovered by now failing run test
|
I think that for now this change is fine. But in the long term, we want to have error recovery wherever possible, so that we can do type-directed autocompletion (e.g. of projector notations). If I see it correctly, the motivating issue for this change was that we didn't fail on errors in run_cmd, right? This will be fixed when we merge #1405. Are there any other reasons to avoid error recovery? |
No description provided.