`agda-mode` Can't Find Executable

Question

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?

• Ryan Luu: Are you using a dev container configuration? If so, then edit that in so we reproduce your question.
• fweth: No, I didn't configure anything. Just create an empty Codespace and install Agda like adviced on the website. Do you have difficulties in reproducing it? If so, I will have another look. I had the assumption that the problem is that the path to Cabal binaries is only in my bash path, but not in the path of VSCode extensions.

Answer 1

I could reproduce the problem. agda works in terminal but extension doesn't find it. I fixed it by opening the settings CTRL + , and searching for agda path

Then under Workspace in Agda Mode › Connection: Agda Path I put /home/codespace/.cabal/bin/agda and then it works

enter image description here

• fweth: Thanks a lot :)

Answer 2

If you think the issue is in the terminal vscode use, you can add to vscode settings under terminal integrated environment:

"terminal.integrated.env.linux": {
 "PATH": "/home/codespace/.cabal/bin:${env:PATH}"
}

Of course with the fitting env.

• fweth: I think this is not it, as I can use Agda in the integrated terminal just fine.