skip to Main Content

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


  1. 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.

    Login or Signup to reply.
  2. 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

    Login or Signup to reply.
Please signup or login to give your own answer.
Back To Top
Search