search

banacorn / agda-mode-vscode

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

Setting agda path to `docker run...` gets ignored, reverts to local CLI #93

Open glangmead opened 2 years ago

glangmead commented 2 years ago

I have agda installed locally and also have created a docker image which I am testing. I set the agda path to docker run -i --rm agda-2.6.2 agda similar to your method here.

But when I try to run agda that way, after a moment my local agda is run instead, and the settings field is erased and changes back to that local agda path (which is in my PATH).

Is my docker command failing, and the plugin is being helpful by falling back to the agda in my PATH?

glangmead commented 2 years ago

I pushed my container to the docker hub, accessible with docker pull glangmead/agda-2.6.2. And here is the Dockerfile.

banacorn commented 2 years ago

Sorry for this late response! But the instruction only works for agda-mode for Atom, which is now archived and not being maintained anymore.

I'll see if we can make Docker work on VS Code!