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

[amblafont]

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):

• Operating system Linus Mint
• coq-lsp version 0.1.8
• VS Code version 1.83.1

[Alizter]

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]

@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]

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]

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.