search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
59 stars 10 forks source link

Idris 2 0.3.0 support #32

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

0.3.0 has just been released, so this issue is a reminder to check what's changed and make sure nothing is broken.

meraymond2 commented 3 years ago

I'm not currently able to run Idris2 0.3.0 with idris2 --ide-mode. I'm getting Uncaught error: (implicit):1:1--1:1:Prelude not found. There was one failed make test during compilation, so I might try rebuilding it. In the meantime, is anyone else able to run it?

zenntenn commented 3 years ago

Idris2 itself seems to be working for me, on Windows 10, compiled in MSYS2.

When I do idris2 --ide-mode I get 000018(:protocol-version 2 0)

I do however still have issue #33

meraymond2 commented 3 years ago

My Prelude bug was unrelated to the new version, it's something to do with the linker paths, which I solved by just compiling it with Nix. The latest is version is out on the unstable channel.

It doesn't look like much has changed in the new release related to the IDE protocol. The only difference my units tests turned up is in the :metavariables response. Premise names previously had 3 empty spaces in front of them for some reason, now they have 2 empty spaces. That doesn't even affect anything, because I apparently still haven't gotten around to adding the premises to the List Metavariables command.