New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support idris2 #132

Open

turion opened this issue Oct 4, 2020 · 4 comments

turion commented Oct 4, 2020

Idris2 is released.It seems this plugin doesn't support it yet?

srid commented Dec 25, 2021

https://github.com/meraymond2/idris-vscode works with Idris2.

michaelmesser commented Feb 12, 2022

https://github.com/bamboo/idris2-lsp-vscode also works with Idris2

ijcd commented Mar 21, 2022

Why so many versions of the same thing? Is there an appreciable difference between how these plugins implement things?

michaelmesser commented Mar 21, 2022

@ijcd
https://github.com/meraymond2/idris-vscode uses IDE-protocol to communicate with idris2
https://github.com/bamboo/idris2-lsp-vscode use LSP to communicate with idris2-lsp

I use the LSP based plugin because it has semantic tokens (better highlighting).

weihongliang233 mentioned this issue

Add newest idris tool chain support calebji123/WordleInIdris#3

Open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment