chore: A crash in the resolver now reports an error to the user

[MikaelMayer]

We don't expect a crash in the resolver, but when I was developing a feature and testing it in VSCode, it would be stuck on "Resolving..." and display no clue that the resolution had crashed.
This PR fixes that, but I don't have a test for it. It did the job in my case.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

This needs a test, especially since we're refactoring this code in #2478. I also wonder whether that PR would already resolve the issue.

[MikaelMayer]

This needs a test, especially since we're refactoring this code in #2478. I also wonder whether that PR would already resolve the issue.

I don't see why #2478 would resolve this issue. Can you please point me to the code that would catch any resolver exception and correctly report it to the user?

[keyboardDrummer]

This needs a test, especially since we're refactoring this code in #2478. I also wonder whether that PR would already resolve the issue.

I don't see why #2478 would resolve this issue. Can you please point me to the code that would catch any resolver exception and correctly report it to the user?

https://github.com/dafny-lang/dafny/pull/2478/files#diff-dc3df6019976d46aad2085bb4506d845f5b0c9c4a717fc07ae1ab0e1fc9f5d71R102

Followed by

https://github.com/dafny-lang/dafny/pull/2478/files#diff-5440b81df3473ec5e681ceb4dd58c934fb240cc819695f5545b57665747f060eR39

[MikaelMayer]

https://github.com/dafny-lang/dafny/pull/2478/files#diff-dc3df6019976d46aad2085bb4506d845f5b0c9c4a717fc07ae1ab0e1fc9f5d71R102

Followed by

https://github.com/dafny-lang/dafny/pull/2478/files#diff-5440b81df3473ec5e681ceb4dd58c934fb240cc819695f5545b57665747f060eR39

That's great indeed, that would do the job. However, you loose the source of the crash (here the resolver). Could you add it as an optional parameter to OnError? That way, I'll be happy and close this PR.

[keyboardDrummer]

That's great indeed, that would do the job. However, you loose the source of the crash (here the resolver). Could you add it as an optional parameter to OnError? That way, I'll be happy and close this PR.

Wouldn't the exception stack-trace that's provided as part for this error provide strictly more information than a MessageSource?

[MikaelMayer]

Wouldn't the exception stack-trace that's provided as part for this error provide strictly more information than a MessageSource?

You get a point there.
In that case, in your PR, could you thus simply parse the stack trace and find whether the error comes from the resolver or the verifier?
I don't have to have one source being called "Crash", because it's not a valid value of MessageSource, so it breaks an invariant.