search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
144 stars 31 forks source link

Coq-lsp doesn't work when filename includes a dash #617

Open amblafont opened 9 months ago

amblafont commented 9 months ago

Describe the bug Coq-lsp doesn't work when the filename includes a dash.

To Reproduce Steps to reproduce the behavior:

  1. Insert a dash in the name of a working Coq file.
  2. Open the file with vscode + coqlsp
  3. See that coqlsp doesn't work (e.g., the goal window remains empty). The first character of the file is underlined in red.

Expected behavior coq-lsp runs sucessfully.

Screenshots

Desktop (please complete the following information):

Alizter commented 9 months ago

Dashes in filenames are not supported by Coq as specified here in the manual: https://coq.inria.fr/refman/practical-tools/coq-commands.html#batch-compilation-coqc. Now that doesn't mean we can't do it for coq-lsp, but my question would be why? You can use underscores instead.

In anycase, coq-lsp should give a good error message and have this limitation documented somewhere.

ejgallego commented 9 months ago

@Alizter is correct, this is a limitation of Coq itself not coq-lsp.

I'm afraid Foo-bar is not a valid library name in Coq, so even if we wanted, it'd be hard to support it without fixing Coq itself first.

I agree we should provide a much better error message, as of now, document creation fails, and the error is reported in the first character as we don't really have a place (yet) to report it better, the message reads:

"Doc.create, internal error: Invalid character '-' in identifier "foo-bar"."

I suggest we wait a little bit to improve this error message until we have the filename to logical resolution logic in place, as that's the right place to validate the filename.

amblafont commented 9 months ago

I see, thanks! It was working with proof general in emacs and it took me some time to realise that the dash was the problem for coq-lsp

ejgallego commented 9 months ago

The message is there, but indeed it is hard to see as Coq fails when trying to create the document.

How does PG handle this case tho? Can it create files containing a dash? If so this is a bug in PG.

I guess what happens in PG is that coqtop is called without the -topfile option, thus a default, dummy library name is used. But that's only a mirage, as that file won't be able to be processed by coqc.

So I guess that is what happened here, and indeed it makes a lot of sense you were puzzled.

For coq-lsp we cannot do that, as we allow to save the current edited file without re-checking it, so we need indeed to use the correct logical name at document creation time.