Implementing errorIDs #3299
Implementing errorIDs #3299
Conversation
Source/DafnyCore/Reporting.cs
Outdated
| @@ -242,7 +236,7 @@ public class ConsoleErrorReporter : BatchErrorReporter { | |||
| errorLine += $" {msg} {TokenToString(tok)}"; | |||
| } | |||
|
|
|||
| if (DafnyOptions.O.CompileVerbose) { | |||
| if (DafnyOptions.O.CompileVerbose && false) { // Need to control tests better before we enable this | |||
There was a problem hiding this comment.
Did you intend to keep this in production? looks like a leftover 🍕
There was a problem hiding this comment.
I wanted to put out error detail when --verbose was true. But many tests have --verbose (equivalently /compileVerbose) true. But you are correct that I forgot about this. But I'd like to deal with it in a subsequent PR, as it may require lots of test changes.
There was a problem hiding this comment.
Took out the block for now.
Source/DafnyLanguageServer/Language/ErrorMessageDafnyCodeActionProvider.cs
Outdated
Show resolved
Hide resolved
docs/check-examples
Outdated
| @@ -118,7 +118,7 @@ do | |||
| ## For header lines, extract the error message from | |||
| ## the header text (everything but the initial ##[ ]* ) | |||
| ( echo "$line" | grep -E -e '[#][#] ' > /dev/null ) \ | |||
| && msg=`echo "$line" | sed -E -e 's/^##[ ]*[*]*//' -e 's/[*]*$//' -e 's/\\*/\\\\*/' -e 's/_[a-z]+_/.*/g'` | |||
| && msg=`echo "$line" | sed -E -e 's/ {#.*}//' | sed -E -e 's/^##[ ]*[*]*//' -e 's/[*]*$//' -e 's/\\*/\\\\*/' -e 's/_[a-z]+_/.*/g'` | |||
There was a problem hiding this comment.
Can you explain me what this change does? At least I would love if there was a change in the comment that reflects what the change on this obscure regex is ^^
There was a problem hiding this comment.
I added a comment in the script. It converts the error message in the header into a regex to match against the eror message produced by running dafny against the example, to be sure the example does what I say.
…nProvider.cs Co-authored-by: Mikaël Mayer <[email protected]>
…into cok-3182-error-id
…into cok-3182-error-id
Fixes #3182
Implementing an error ID in order to enable showing the user more detailed error explanations and quick fixes.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.