Restoring the old error handler in Errors.catch_errors_aux #2965
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.
FStar.Errors.catch_errors_aux is used to trap errors that can be raised in a function and to return back any issues rather than adding them to the default error handler. However, in case the error raised was a fatal error (e.g., Failure), then this function would not restore the original error handler, leading to very confusing behavior at the top-level, e.g., a tactic could fail saying issues were reported, but actually none would be reported. With Guido, we fixed this so that this function always finally restores the original error handler.
Additionally, in FStar.Tactics.Basic, in the functions that provide user-facing callbacks to the typechecker, we also trap fatal errors (e.g., violation of locally nameless convention) and return them to the caller as issues.
This addresses problems as seen in FStarLang/steel#17