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

[Liang-Ting Chen]

Dear Jesper,

Yes. Managing issues seems fine to me (when I am not busy with paper
writing).

As I am not so familiar with Reason and TypeScript, it will be nice to have
someone fluent in these language to review PRs carefully.

Best wishes,
Liang-Ting

On Tue, Jul 25, 2023 at 20:46, Jesper Cockx <J.G.H.Cockx at tudelft.nl> wrote:

> 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
>
-- 
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/426a7e0a/attachment.html>