Michael Soegtrop (Oct 17 2022 at 09:14): Michael Soegtrop (Oct 17 2022 at 09:14):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.
Karl Palmskog (Oct 17 2022 at 09:20):VSCodium uses the Open VSX store. The extension needs to be registered in that store to appear inside VSCodium
Karl Palmskog (Oct 17 2022 at 09:20):for example, here is VsCoq in Open VSX: https://open-vsx.org/extension/maximedenes/vscoq
Enrico Tassi (Oct 17 2022 at 10:47):Is it a full upload or just a link?
Enrico Tassi (Oct 17 2022 at 12:05):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.
Enrico Tassi (Oct 17 2022 at 12:35):OK, the packages should be visible, but I did not test them
Enrico Tassi (Oct 17 2022 at 12:35):gares.elpi-lang and gares.coq-elpi-lang
Michael Soegtrop (Oct 17 2022 at 13:23):@Enrico Tassi : thanks it works for me - I can install it and I see the code highlighting!
Michael Soegtrop (Oct 17 2022 at 13:23):Indeed VScodium was a mess when they made this store switch, but this rectified quite quickly. I would say it is fine again.
Enrico Tassi (Oct 17 2022 at 15:01):elpi-lang now also provides a trace browser, which also works inside coq, but I did not document it yet
Enrico Tassi (Oct 17 2022 at 15:03):I hope I'll find some time soon
Last updated: Oct 13 2024 at 01:02 UTC