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

[Liang-Ting Chen]

Hi,

I realised that there are other repositories (currently maintained by Ting-Gian
Lua) on which the VS code extension depend, so transferring the repository
for the extension alone won’t work.

Lua’s availability is limited now as he is in the industry, but he will
participate the next AIM. I hope we can get the takeover done during AIM
and we can discuss what else should be implemented, such as more LSP
features (currently broken, if I am not mistaken). Some changes need to be
made in Agda’s codebase, though.

[ A working VS Code extension is very handy at least for teaching, as I
don’t know any student using Emacs regularly. Hope we can keep this
extension maintained and even enhanced. ]

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

https://l-tchen.github.io


On Tue, Jul 25, 2023 at 21:20, Liang-Ting Chen <liang.ting.chen.tw at gmail.com>
wrote:

> 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/20230910/3d817cb0/attachment.html>