feature request: Add scratch pad

[Alizter]

Sometimes during development you may come across a Coq bug which you need to make an example for. My current workflow is to make a new file called bug.v and play around in there. However this requires saving the file and can pollute the source tree if forgotten about.

Would it be possible to have a *scratch* buffer like exists in CoqIDE and emacs where the user can write some Coq without having to save.

[ejgallego]

I think that's possible, nothing in coq-lsp requires you to save the file, right?

We could add a command for that, but how would it be different from just creating bug.v and not saving it?

[Alizter]

It doesn't appear as though coq-lsp starts without saving the file.

[ejgallego]

I think that's VSCode choice, not ours. Makes kind of sense tho as it wants to pass to the server a file:/// uri.

So indeed I don't see a way for coq-lsp to override this behavior in VSCode.

[ejgallego]

We can implement other URI schemes if we would have a need, but we'd need a client for them first.

[Alizter]

I suppose then there is not much we can do about this.

[ejgallego]

I am not sure, just trying to figure out, I don't see a way but there could be one. I think they are 3 actions actually that can be done:

• in the VSCode front, maybe open an issue to see if that would be possible
• in LSP front, ask for clarification about what URI schemes are supported
• in the coq-lsp server front, we could support an ephemeral:/// uri, that actually makes a lot of sense, maybe not for VSCode, but for sure other clients like machine learning and linter may want to use that kind of URIs
  • They also have a need for forking a document efficiently, as to perform search, SerAPI did implement something like this, but I'm unsure if the clients ever got to use it.

There is also the question if it is possible to implement a VSCode command "open scratch buffer", maybe it is, but we'll have to dig into the concrete VSCode API hooks that BaseLanguageServer client is using to trigger didOpen.

[ejgallego]

The feature in principle seem sensible to me

[4ever2]

I suppose then there is not much we can do about this.

This is definitely possible, probably even easy to do. Unsaved files have the URI scheme untitled and you can easily configure the language client to start on Coq files with that scheme.

The only problem that I see is that untitled documents don't have a file extension, so coq-lsp might reject it.