If I understand this right there is an ELPI plugin for VSCode - as VSCodium user I don't see it in the store. I don't know the details but afaik there is a MS managed store and a community managed store and VSCodium (without some hacks) accesses only the latter one. The VSCoq plugin is visible in VSCodium, so maybe you can ask them how they did it.
VSCodium uses the Open VSX store. The extension needs to be registered in that store to appear inside VSCodium
for example, here is VsCoq in Open VSX: https://open-vsx.org/extension/maximedenes/vscoq
Is it a full upload or just a link?
Very boring, I claimed the namespace and signed bla bla agreements, I guess I'll evntually manage to upload.
FTR I used to be a vscodium user, and I quit when the main store stopped working out of the box.
OK, the packages should be visible, but I did not test them
gares.elpi-lang and gares.coq-elpi-lang
@Enrico Tassi : thanks it works for me - I can install it and I see the code highlighting!
Indeed VScodium was a mess when they made this store switch, but this rectified quite quickly. I would say it is fine again.
elpi-lang now also provides a trace browser, which also works inside coq, but I did not document it yet
I hope I'll find some time soon
Last updated: Feb 04 2023 at 02:03 UTC