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

Inconsistencies with Loc in coqc and vscoq #950

Open
gares opened this issue Nov 29, 2024 · 4 comments
Open

Inconsistencies with Loc in coqc and vscoq #950

gares opened this issue Nov 29, 2024 · 4 comments

Comments

@gares
Copy link
Member

gares commented Nov 29, 2024

Here the problem: it seems that the ranges written in the terminal and the ranges sent via lsp are 1-based v.s. 0-based.


In this case I clicked on the error location as printed in the terminal, and code selects the exact text:

Screenshot from 2024-11-30 16-41-28


Here I peek the lsp traffic for the same error. The line number was decreased by 1, so I guess it is zero based.
The column numbers are the same, so (assuming they are also 0 based)< are coloured 1 char to the right.

Screenshot from 2024-11-30 16-40-50

@gares gares closed this as completed Nov 29, 2024
@gares gares reopened this Nov 30, 2024
@gares
Copy link
Member Author

gares commented Nov 30, 2024

I don't know exactly why, but it seems the loc I generate are OK for coqc, but get somehow shifted by vscoq.

@SkySkimmer
Copy link
Contributor

Is this only with elpi stuff or can you reproduce with something simple like Check doesntexist.?

@gares
Copy link
Member Author

gares commented Dec 1, 2024

I think it is only elpi, but also only with code, since with coqc locs are ok

@rtetley
Copy link
Collaborator

rtetley commented Dec 4, 2024

So we compute the lsp range using the Loc.t from Coq via:
https://github.com/coq/vscoq/blob/96b677a32d43dfd9ce7aa2a9f1ac7480477b0f2e/language-server/dm/rawDocument.ml#L83C1-L87C4

Looking at the code we seem to use loc.bp and loc.ep from the type:

type t = {
  fname : source; (** filename or toplevel input *)
  line_nb : int; (** start line number *)
  bol_pos : int; (** position of the beginning of start line *)
  line_nb_last : int; (** end line number *)
  bol_pos_last : int; (** position of the beginning of end line *)
  bp : int; (** start position *)
  ep : int; (** end position *)
}

Other than that it does indeed seem to be 0 based. Maybe there is a difference in how you instantiate bp and ep but not other members of that record which lead to the inconsistencies ?

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 a pull request may close this issue.

3 participants