agda-mode-vscode
agda-mode-vscode copied to clipboard
load (c-c c-l) is stuck with "Loading .."
I had vs code with agda-mode working - installed following instructions on a system build with debian and using cabal. Then I deleted the .cabal/store folder (it had accumulated too much old stuff) and rebuild anything I remembered, including cabal install for agda-mode producing als executable.
After removing and (re-)install of agda-mode in VS Code, the load command was available, but showed only "Loading ..." but did not advance. After several repeats of disable, uninstall, install... eventually the agda-mode worked again correctly.
What is the proper sequence of completely reinstall agda-mode? Could you include a bit more information, where stuff is cached, to understand which steps are needed? Thank you for a very nice tool!
I think the only proper way of reinstalling agda-mode (specifically, the editor extension itself, not including agda or als), is by clicking uninstall and then install in Extensions, nothing fancy really.
agda and als installed via stack or cabal is also pretty standard (please don't ask me how).
However, als installed by agda-mode is a different story, because it's downloaded by agda-mode when it cannot find agda nor als in PATH. The downloaded artifacts are stored in ExtensionContext.storagePath, I'll close this issue when there's a command for clearing those artifacts.
For some reason, the uninstall and install sequence did not work. I assume there is somewhere something left in the uninstall step, What is necessary after the uninstall to finalize it? closing VS Code? just a restart? I had 'agdaand laterals` in my my search PATH. Perhaps it was some process which took a while to clean or reconstruct something?
In any case, in the end it worked again. Thank you for looking into it!
I'm stuck on this issue as well now! I tried poking around through the output windows in VSCode but didn't find anything noteworthy. How to debug what's wrong?
[Edit] Just got it working again by disabling the Language Server.
Same issue, running the binary /usr/bin/als gives no unexpected error
Got hit by the same issue. Trying to use ALS with the v0.3.11 of agda-mode resulted in an endless "Loading ...", while the Emacs connection worked correctly. After checking the VSCode logging panels, I noticed that the error described in #116 was in there (see below). After downgrading to the v0.3.9 of agda-mode (as suggested in the linked issue), the ALS connection ended up firing correctly.

Maybe those two issues are actually the same in the current version of this extension?