I installed Agda in Codespaces via Cabal, the installation seems to run fine, I can also use Agda in the integrated terminal, but the extension agda-mode
gives me this error:
Connection Error: Unable to find agda
Here are the error messages from all the attempts:
Trying to locate "" but the file does not exist
Trying to find the command "agda": Cannot find the executable on PATH
The installer loaded /home/codespace/.cabal/bin
into my path, I think via some bash config file, but I assume the extension is not running bash? How can i put the cabal folder into the extension’s path?
2
Answers
If you think the issue is in the terminal vscode use, you can add to vscode settings under
terminal integrated environment
:Of course with the fitting env.
I could reproduce the problem.
agda
works in terminal but extension doesn’t find it. I fixed it by opening the settingsCTRL + ,
and searching foragda path
Then under
Workspace
inAgda Mode › Connection: Agda Path
I put/home/codespace/.cabal/bin/agda
and then it works