Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: print error context snippets after their messages #4788

Merged
merged 2 commits into from
Nov 16, 2023

Conversation

alex-chew
Copy link
Contributor

Description

Fixes #4787.

How has this been tested?

Added git-issue-4787.dfy to test the reported case.

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

@alex-chew alex-chew changed the title fix: print error contexts after their messages fix: print error context snippets after their messages Nov 16, 2023
@alex-chew alex-chew marked this pull request as ready for review November 16, 2023 01:02
@@ -66,14 +66,14 @@ public class ConsoleErrorReporter : BatchErrorReporter {
errorLine += "\n";
}

Options.OutputWriter.Write(errorLine);

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The fact that this was fixed by changing the core message reporting code makes me think that some of the other messages (which already came before the snippet) aren't using this and maybe should be? Not that we need to fix that now, it's just an inconsistency we might want to resolve at some point.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, I didn't get a chance to search for where the other messages (like normal verification failures) were bring printed from, but it's a good idea to unify them to use this logic.

@alex-chew alex-chew merged commit 1b89c34 into dafny-lang:master Nov 16, 2023
20 checks passed
@alex-chew alex-chew deleted the fix/issue-4787 branch November 16, 2023 17:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Redundant- and contradictory-assumptions warnings are incorrectly formatted
2 participants