search

banacorn / agda-mode-vscode

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

Connection Error: Internal Parse Error #75

Closed barrettj12 closed 2 years ago

barrettj12 commented 2 years ago

Whenever I try and load any file (C-c C-l), I get the following (very opaque) error:

Connection Error: Internal Parse Error

Parse error code: R0 ""Agda""

despite the fact that Agda compilation works fine from the command line.

barrettj12 commented 2 years ago

Okay, so it turns out that the Agda path was wrong in the extension's settings, and this was causing the problem. Still, it would be nice to have a more informative error message

banacorn commented 2 years ago

Which version of Agda are you using?

barrettj12 commented 2 years ago

A recent development version (agda/agda@6cb77e1)

banacorn commented 2 years ago

I see, the protocol has changed!