[Agda-dev] Takeover of Agda mode for VS Code?

[Jesper Cockx]

Dear Liang-Ting,


Thank you very much for taking initiative on this! I think it would be best to open up this discussion to include the other developers into this discussion, so I'm forwarding this to the agda-dev mailing list.


Personally, I think it would be great to have agda-vscode under the Agda organization, though it would also be good to have someone not already in the core developer team take primary responsibility for managing issues and reviewing PRs. Is that something that you'd be willing to do yourself?


Best regards,

Jesper



________________________________
From: Liang-Ting Chen <liang.ting.chen.tw at gmail.com>
Sent: Tuesday, July 25, 2023 10:25:27 AM
To: Jesper Cockx
Cc: 賴廷彥
Subject: Takeover of Agda mode for VS Code?

Hi Jesper,

I hope this message finds you well. I have recently been in discussion with Ting-Gian Lua (a.k.a. banacorn on GitHub, cc'ed) regarding his VS Code extension for Agda (https://github.com/banacorn/agda-mode-vscode). He is happy to transfer ownership of the extension to the Agda community. Now, the question is if the Agda dev team wants to take it over and how we should transfer.

As of now, there are no official ways for transferring ownership but two viable options:

Option 1 is to continue using Ting-Gian LUA as the publisher of the extension.
Option 2 is to deprecate the current extension and republish it under the publisher name "agda".

Regardless of the option we choose, once the CI integration is done, only the "personal access token" will need occasional updating so that the extension can be published directly from the GitHub repository.

Do you think the Agda team has enough workforce to take it over? I have some time to look after his extension this summer.

Looking forward to your input.

Cheers,
Liang-Ting

--
Dr Liang-Ting Chen
Institute of Information Science
Academia Sinica, Taiwan

https://l-tchen.github.io
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20230725/8948b69d/attachment.html>