-
Notifications
You must be signed in to change notification settings - Fork 152
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
Print source lines in error messages #2517
Conversation
10a59ff
to
bb9f952
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there is a off by one error here. The ending location in K points to the next character after a token, so that when you select a piece of code, the location matches with what your editor is telling you.
The correctness of this is debatable, but I think it makes it easier to find the location of the problematic code in your editor.
@@ -1,7 +1,11 @@ | |||
[Error] Inner Parser: Parse error: unexpected token '[' following token '('. | |||
Source(nestedFunctionContextInFun.k) | |||
Location(8,16,8,17) | |||
8 | rule 0 => #fun([[0 => 1]] <bar> 0 </bar>)(0) | |||
. ^~ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This doesn't look right.
The error message says only one character is of blame here, but the underline shows two.
The location information for K is an interval that is inclusive on the left, and exclusive on the right: [0,1)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
hey I looked at this closer and i think it's correct in that the error message underlines the location. If there's only one incorrect character, the location should be (8,16, 8, 16) but somehow, the lexer is picking up two characters.
See the following diff which is a part of this PR.
diff --git a/k-distribution/tests/regression-new/checks/tokenCheck.k.out b/k-distribution/tests/regression-new/checks/tokenCheck.k.out
index eb2f33f4b1..b3f85ac44c 100644
--- a/k-distribution/tests/regression-new/checks/tokenCheck.k.out
+++ b/k-distribution/tests/regression-new/checks/tokenCheck.k.out
@@ -1,7 +1,11 @@
[Error] Compiler: Sort X was declared as a token. Productions of this sort can only contain [function] or [token] labels.
Source(tokenCheck.k)
Location(10,16,10,21)
+ 10 | syntax X ::= fail()
+ . ^~~~~~
[Error] Compiler: Sort Y was declared as a token. Productions of this sort can only contain [function] or [token] labels.
Source(tokenCheck.k)
Location(13,16,13,16)
+ 13 | syntax Y ::= Z
+ . ^
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Both of these show terms parsed by the outer parser.
It seems we may have some sort of inconsistency.
At the time of writing, error messages display location information like so: ``` [Error] Compiler: Found existential variable not supported by concrete backend. Source(/home/erik/error/test.k) Location(11,39,11,41) ``` Sometimes these messages can be difficult to decipher due to the lack of information from the actual source code. Add this information in the error message so that the errors look like this: ``` [Error] Compiler: Found existential variable not supported by concrete backend. Source(/home/erik/error/test.k) Location(11,39,11,41) | rule <k> a => b ... </k> requires ?_ ==Int _ | ^~ ``` For longer lines, error messages look like this: ``` [Error] Compiler: Claims are not allowed in the definition. Source(/home/erik/error/test.k) Location(15,11,17,13) . v 15 | claim _ 16 | => 17 | . . ~~^ ``` If error messages span more than 3 lines, the lines between the first and last line are replaced with a single line containing `...` to avoid taking up too much space on the terminal.
d2bdf4f
to
7be37b0
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is looking way better than I originally imagined.
…untimeverification#1886) * haskell-backend/src/main/native/haskell-backend: c160d484 - Update evm test generation script (runtimeverification#2513) * haskell-backend/src/main/native/haskell-backend: e4457b23 - Update dependency: deps/k_release (runtimeverification#2512) * haskell-backend/src/main/native/haskell-backend: 38dd2e25 - Avoid detached HEAD in Update workflow on push events (runtimeverification#2517) * haskell-backend/src/main/native/haskell-backend: 47bfdc78 - Update dependency: deps/k_release (runtimeverification#2519) * haskell-backend/src/main/native/haskell-backend: 7b1a0bde - kore-repl: improve exception handling (runtimeverification#2514)
…untimeverification#1898) * haskell-backend/src/main/native/haskell-backend: c160d484 - Update evm test generation script (runtimeverification#2513) * haskell-backend/src/main/native/haskell-backend: e4457b23 - Update dependency: deps/k_release (runtimeverification#2512) * haskell-backend/src/main/native/haskell-backend: 38dd2e25 - Avoid detached HEAD in Update workflow on push events (runtimeverification#2517) * haskell-backend/src/main/native/haskell-backend: 47bfdc78 - Update dependency: deps/k_release (runtimeverification#2519) * haskell-backend/src/main/native/haskell-backend: 7b1a0bde - kore-repl: improve exception handling (runtimeverification#2514) * haskell-backend/src/main/native/haskell-backend: ff35eb73 - Update dependency: deps/k_release (runtimeverification#2524) * haskell-backend/src/main/native/haskell-backend: 85800442 - Export prelude.kore in Nix (runtimeverification#2522) * haskell-backend/src/main/native/haskell-backend: 32d6090b - Add a script to time execution steps (runtimeverification#2527) * haskell-backend/src/main/native/haskell-backend: ac340731 - Update dependency: deps/k_release (runtimeverification#2534)
At the time of writing, error messages display location information like
so:
Sometimes these messages can be difficult to decipher due to the lack of
information from the actual source code. Add this information in the
error message so that the errors look like this:
For longer lines, error messages look like this:
If error messages span more than 3 lines, the lines between the first
and last line are replaced with a single line containing
...
to avoidtaking up too much space on the terminal.