Shorten rocq-lsp

[gares]

This PR does two things:

• use the current name of the opam package for vscoq-language-server
• makes the rocq-lsp entry not-a-copy of the vscoq one, and makes it sensibly shorter.

Given there is another page on how to install vscoq, we could short that section as well and link to that tutorial.

[Zimmi48]

Given there is another page on how to install vscoq, we could short that section as well and link to that tutorial.

What other page? Are you talking about the one that was removed as part of #59?

[Zimmi48]

I'm fine with merging these changes, but:

• they should be done for all the OS (currently only done for one)
• so far, the way things have been done on the website is to link to future things that do not exist yet (lots of broken URLs). Given that Rocq 9.0+rc1 is out anyway, won't the vsrocq-language-server opam package be released relatively soon?

[gares]

Oh, didn't notice the instructions were per-OS. fixed.

I let @rtetley comment on the package (re)name

[rtetley]

The plan was to do a release in two weeks. But there is nothing set in stone, we could always proceed earlier if necessary.

[gares]

And that release could have the new name (opam side) and we could have an empty package just depending on the new one to not break user's setup.

At the same time, I don't know how to handle the transition in the app store, would the same strategy work?

[Zimmi48]

At the same time, I don't know how to handle the transition in the app store, would the same strategy work?

On the app store, it's time not to call this extension maximedenes.vscoq anymore.
A rocq-prover organization should be created first. Then, then extension can be called rocq-prover.vsrocq. I guess it should be fine to keep publishing it in both places, or you can just mark maximedenes.vscoq as deprecated and stop updating it.

[rtetley]

I already created the organisation to prepare for this. Indeed deprecating the old one is a solution but we lose the download stats and ratings

[Zimmi48]

Otherwise, is there support from transferring and renaming in the VS Code marketplace? If yes, that would likely be the best option.

[rtetley]

So from my research, I could theoretically contact vscode marketplace support team and rename the extension. This what would happen though (from this stack overflow thread):

The download stats would remain same even after the extension transfer. Usually, we do not allow transfer of VSCode extensions since it has following consequences:

1. Users will not be able to install the older versions of your extensions that got published before the extension transfer from the VSCode.
2. If this extension is used as a dependency in other extensions by using publisherName.ExtensionName, that would not work.
3. You need to update all references to this extension with the new publisherName.

I will still contact support and see.

[Zimmi48]

To me, it looks like points 2 and 3 are not an issue. Point 1 is indeed an issue, but it could be worked around by re-publishing all the past versions.

[rtetley]

Well I contacted vscode marketplace support, they suggested we deprecate the extension. See: microsoft/vscode-discussions#1

I am not sure they change the publisher name anymore :-/

[Zimmi48]

Well, I think this solution is fine as well. Statistics on the new extension will go up fast again. Especially with the previous extension deprecated and pointing to the new one.