Unicode input

[Alizter]

It would be good to have a mechanism like CoqIDE has where you can press \ and then type in a unicode character name. It is possible to use extensions to insert unicode characters, but they don't appear in the completion interface.

[ejgallego]

It is possible to use extensions to insert unicode characters, but they don't appear in the completion interface.

That should be fixed by these extensions, shouldn't it?

I'm unsure this is something that coq-lsp should mess with, it seems to me that unicode input is something global for a particular editor, and should work uniformly over all files.

[Alizter]

Its not coq-lsp who should do something about this, but rather the vscode extension.

[ejgallego]

I don't see why the coq-lsp vscode extension should mess with this.

[Alizter]

I think its something that will make the user experience nicer, but not something we should focus on.

[ejgallego]

I'm unsure a coq-lsp specific unicode input mode is going to make the user experience better or more confusing, as now users see their preferred unicode input method working / conflicting with the one in coq-lsp.

A coq-specific input mode would be a great thing to have, but unicode seems wide scope for me, and the bug you point out of current unicode extensions not integrating with completion can be fixed by the extensions themselves, in fact I'm surprised there is not extension in the marketplace that will contribute a completion provider.

jsCoq or CoqIDE have these niceties, but note that this is something done at the editor level (I myself wrote the CodeMirror plugin for it in jsCoq) , not in the Coq-specific part.

So this IMHO goes beyond the "not something we should focus on" to something we'll reject to merge, unless there is some really Coq-specific needs relating unicode input.

[Alizter]

I think providing an optional unicode input method in the VSCode extension is a worthwhile feature. We should at the very least make note of recommended extensions / fixes for completion. Try writing Greek letters in a Coq file you are editing in VSCode with coq-lsp. I have not yet been able to come up with a good workflow, other than copy and pasting.

[ejgallego]

I have little experience with VS Code, and indeed good unicode input is essential these days; I'm not sure how it is supposed to work with VS Code, indeed a pointer to the current best practices would be great.

I still don't see why coq-lsp has to be in charge of that, even in jsCoq I put it under its separate extension.

Why is unicode input specific to coq-lsp again?

By the way, would we decide to implement this, that would be a server feature as it is the completion call that would need to be extended with the unicode symbols.

Doing it client-wise would be silly as it would amount to a fully independent extension on their own.

I would also not be surprised if the current unicode extensions for VS Code are bad and we'd like to write our own, but for sure that's better done as a separate extension that contributes a completion provider to all text buffers.

[Alizter]

Why is unicode input specific to coq-lsp again?

Every editor (for every proof assistant I know) provides a way of inputting unicode values specific to them.

By the way, would we decide to implement this, that would be a server feature as it is the completion call that would need to be extended with the unicode symbols.

I'm not at all suggesting we modify the LSP. This is really a quality-of-life feature of the extension itself.

Doing it client-wise would be silly as it would amount to a fully independent extension on their own.

Yes that is perhaps silly, only if there exists an extension today that can do it. If that is not the case, we should develop and recommend our own.

[ejgallego]

Every editor (for every proof assistant I know) provides a way of inputting unicode values specific to them.

I'm not at all suggesting we modify the LSP. This is really a quality-of-life feature of the extension itself.

Umm aren't these two things really at odds? If unicode input is kind of essential we could have the serve take care of that, and then you get support in all editors for free.

Every editor (for every proof assistant I know) provides a way of inputting unicode values specific to them.

Maybe they do, I don't know them all (for emacs I actually use unicode-input-mode, for other apps I use the GTK unicode input method)

But even if all editors do that, it seems like a really bad thing to do, instead of relying on the unicode input system provided by the editors. It seems really strange to me that I could only input \alpha in .v files and not in the README or in .json files for example.