agda is running in read-only (sandboxed?) filesystem

[cspollard]

Hello,

First, let me thank you for writing and maintaining this extension: agda would be very difficult without it.

I've noticed that system calls via the Reflection.External interface fail if they try to alter any files. I suspect this is due to a vscode sandbox for extensions. I think it must be possible for extensions to touch files though (otherwise I'm not sure how e.g. the latex extension works).

Minimal example:

Type checking

module _ where

  open import Reflection.External
  open import Data.String using (String)

  touch : String → CmdSpec
  touch s = cmdSpec "touch" [ s ] ""

  test : String
  test = runCmd (touch "hello")

yields

Error while running command 'touch hello'
Input:

Output:

Error:
touch: hello: Read-only file system

when checking that the expression unquote (runCmd (touch "hello"))
has type String

Is it possible to enable write-acess to the local filesystem?

Chris

[cspollard]

Hi.

Just to say, I'd be happy to help here if I can -- fixing this would be very helpful for my workflow. I don't have much experience with javascript or rescript, but if it's not a huge change I can try to learn...

Chris

[cspollard]

Hi,

I've been looking into this in more detail. The issue is that when agda is run standalone from a shell, shell commands called via reflection are (correctly?) called from the working directory of the shell. When called via agda-mode-vscode, the working directory is /.

To be fair, maybe it's not obvious where relative paths should point, but I suppose vscode has a concept of a project directory: perhaps they could use this as the working dir?

Chris

[L-TChen]

Sorry for the late reply. Yes, VS Code does have something called a ‘project root’ or ‘workspace folders’, which you can find more details in https://code.visualstudio.com/docs/editor/workspaces.

I believe the working directory is set somewhere, and you should be able to point it to the project root. I'm not familiar with the codebase right now, so it might take me a bit of time to locate it.

If you'd like to help with this, your PR would be greatly appreciated. 🙂