Processing Coq sources extracted from .rst/.md files

[cpitclaudel]

Hi Emilio!

When I compile a literate reST or Markdown document with Alectryon I start the LSP server with a filename ending in .rst or .md (since that's what I have on disk), but the contents are plain Coq source code (all markup has been removed). coqlsp doesn't like that:

Error in document conversion: unknown file format

Is there a way for me to tell CoqLSP that the input is Coq code, even if it comes from a .md or .rst file?

Thanks a lot!

[ejgallego]

I'm not sure how to implement this without breaking the existing .md workflow. Indeed, file extension is used to determine the top-level parser, so a markdown file needs to have ````coq` entry for it to work.

Would it be a big issue to name the file foo.md.v ?

(Note that using LSP, the file doesn't need to exist on disk.)

[cpitclaudel]

Would it be a big issue to name the file foo.md.v ?

It would be a big issue to rename it on disk (because it's not a Coq file), but I can certainly adjust the name that I send to CoqLSP; good idea! I will try that.

[ejgallego]

I've checked the LSP spec and actually there is a languageId parameter in the didOpen notification which can be used to specify the language the file is on.

This parameter is ignored (for historical reasons), but indeed, I propose to fix this problem so you can just specify the languageId you want, regardless of the extension.

[cpitclaudel]

That's a great idea!