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

[glangmead]

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]

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

[banacorn]

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!