Error message location messed up in the presence of CRLF

[4ever2]

For files with CRLF line endings VsCoq computes error locations incorrectly.

With Coq <= 8.14 the error start location is one character off if there is at least one \r in the sentence.
With Coq >= 8.15 the error start location is off one character for each \r in the sentence.

[thery]

is it a coq issue or a vscoq one?

[4ever2]

The behavior observed with >= 8.15 is a vscoq issue, likely due to coq/coq#14767.

Before 8.15, coq would remove \r from XML input, so vscoq compensates for that when converting offsets to positions. The code doing this conversion is:
https://github.com/coq-community/vscoq/blob/146c267e511dc58581a358286e778d4acd195e0b/server/src/util/text-util.ts#L218

[thery]

why is it not simply

    currentOffset+= match[0].length;
    offset -= match[0].length;

?

[thery]

still I don´t understand why the error is one character independently of the number of lines

[4ever2]

why is it not simply

    currentOffset+= match[0].length;
    offset -= match[0].length;

?

That would probably work for coq >= 8.15.0 but not for older versions.

[thery]

I've tried with 8.13 and 8.16 it both seems to work

[thery]

no it works only with 8.16

[4ever2]

The off-by-one error with Coq 8.14 and earlier seems to be a Coq issue.
Given the statement \r\n\r\n\r\nTest a., Coq will return an offset of 4, which is clearly wrong.
coq/coq#14767 states that Coq removes carriage return by converting \n\r to \r. This would explain why Coq returns an offset 4 since the sentence would be transformed to \r\n\n\nTest a.

[thery]

What I don´t understand is that the fix of vscoq seems to count \r\n as one. So the deviation could be more than one if you give
\r\n\r\nCheck 1 \r\n\r\n + foo.

[4ever2]

The deviation of the error start position cannot be more than one since the second \r left would be after the offset.
But in your example the error end position would be two characters off.

[thery]

the error is that foo is not defined so we have a shift of 2.

[4ever2]

The obvious fix would be to change the regex to look for \n\r, but I'm unsure if that would break something else.

[thery]

I think we should make the change

offset -= match[0].length;

to make the error for window works for coq >= 8.15

[4ever2]

But doesn't that make the problem worse for coq <= 8.14?

I implemented a different fix for the coq >= 8.15 problem in 4ever2@33eead0 but your fix is definitely cleaner.

[thery]

This seems to work for <= coq 8.14

    const lineEndingRE1 = /([^\r\n]*)((\r\n)*|\r|\n)?/;
    
    ...
    
    const match = lineEndingRE1.exec(text.substring(currentOffset));
    // match[0] -- characters plus newline
    // match[1] -- characters up to newline
    // match[2] -- newline (\n, \r, or \r\n)
    const value = match[0].length - match[1].length;
    if(!match || match[0].length === 0 || match[1].length >= offset)
      return Position.create(line, lineOffset + offset)
    currentOffset+= match[0].length;
    offset -= match[1].length + (Math.floor(value / 2)  + 1);
    lineOffset = 0;
    line += Math.floor((value + 1) / 2);

[4ever2]

Yes, that seems to work well.

[thery]

I have only two worries:

• I am testing this on linux doing a sed to turn my linux file into a window one. I would like to be sure it works on native windows.
• The function (..CLN) that is modified is called at 2 places: STM and State.
  Does your change on STM should also be reflected in State?

[4ever2]

I am testing this on linux doing a sed to turn my linux file into a window one. I would like to be sure it works on native windows.

I tested this on Windows. Instead of using sed you can also force VS Code to use CRLF when testing.

The function (..CLN) that is modified is called at 2 places: STM and State.

I tried changing it in State and couldn't observe any difference, so I am unsure what should be done there.

[thery]

One of them seems about warning. So for example deprecation is a warning. In 8.14,

\r\n\r\n\r\nHint Resolve id.

the location seems ok?

[4ever2]

Warnings don't contain error locations so I don't think that code is reachable.

[Blaisorblade]

Warnings don't contain error locations so I don't think that code is reachable.

Maybe that is true, but warnings contain warning locations so that sounds strange — shouldn't positions be adjusted the same way?

Either way problems seem to remain. On VsCoq master (plus #319) with Coq 8.16, CRLF line endings, this code:

seems to have an off-by-2 on the error but not the warning:

I'm (tentatively) reopening.

EDIT: My bad sorry, my VsCoq checkout was one commit behind.

[Blaisorblade]

Really, the warning is off-by-one since highlighting starts at the line end, but that happens without CRLF as well so that is probably separate. (I haven't compared what Coq does and/or other IDEs).

[4ever2]

The warning is off-by-one since warnings don't seem to contain locations (they only contain state ID) so VsCoq will highlight the entire sentence.

Strangely, the error message in your example is correct on my machine with CRLF and coq 8.16.

[thery]

Strangely, the error message in your example is correct on my machine with CRLF and coq 8.16.

me too

[Blaisorblade]

After pulling I agree, my bad!