search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Refactor conditions to enable shortcuts #140

Closed pimotte closed 1 year ago

pimotte commented 1 year ago

Fixes #132

jespercockx commented 1 year ago

@banacorn Would it be possible to please merge this PR? Or alternatively, could you give me (or someone else within the Agda dev team) permission to merge PRs here?

GUIpsp commented 1 year ago

Hello, I also had trouble with this behaviour. I took the liberty of publishing an extension with this fix, because otherwise it can be difficult to install in remote vscode.

It is available here: https://marketplace.visualstudio.com/items?itemName=GuilhermeEspada.agda-mode-fork Let me know if there is any other things I should merge into it.

Espada

L-TChen commented 1 year ago

I will contact him privately. Please hold for a moment.

L-TChen commented 1 year ago

I am able to merge this PR now (@jespercockx may also have received the invitation to own this repo as well), but I am not familiar with VS code extension development.

Is there anything I need to do after merging this PR to update this extension?

pimotte commented 1 year ago

I would follow this procedure:

Looking at https://github.com/banacorn/agda-mode-vscode/blob/master/.github/workflows/release.yml that's all it seems to need

This will also publish an updated version to the VSCode marketplace

GUIpsp commented 1 year ago

Hey, happy to see the original repo brought back.

You might need to remove the svg from the readme before you are able to publish. I had to this

Espada

L-TChen commented 1 year ago

@GUIpsp what did you mean by removing the SVG from the readme..?

GUIpsp commented 1 year ago

MS banned svg images from their readmes out of security concerns. This may be project/tool specific, but I had to remove them to publish the fork. Look here: https://github.com/GUIpsp/agda-mode-vscode/commit/a65d0975f1b347f0d6d8627027512a3e693c4e51#diff-b335630551682c19a781afebcf4d07bf978fb1f8ac04c6bf87428ed5106870f5L3

L-TChen commented 1 year ago

Right, thanks for letting me know!

L-TChen commented 1 year ago

All done. Just waiting for the CI to complete.

ncfavier commented 1 year ago

Looks like we'll need @banacorn to refresh the Personal Access Token to the vscode marketplace.

Also, you might want to bump publish-vscode-extension to v1 to get rid of this warning. EDIT: and checkout to v3.

GUIpsp commented 1 year ago

Is it viable to move this to the Agda organization? It's probably good we don't burden @banacorn with extra maintenance burden.

jespercockx commented 1 year ago

I would be very happy to move this into the Agda organization! Do you know if it's possible to move a repository on github or do we need to create a new repo?

ncfavier commented 1 year ago

https://github.com/banacorn/agda-mode-vscode/transfer

I don't know if it's possible to transfer the vscode extension to another publisher though.

L-TChen commented 1 year ago

I will discuss this with @banacorn when he is available and see how to proceed.

ncfavier commented 1 year ago

This is still not published.

L-TChen commented 1 year ago

0.3.12 should now be published. I now have permission to manage the extension and will try to maintain it on behalf of @banacorn at least before we officially transfer this extension to the Agda development team.