Fails on nixos

[wldhx]

With

/nix/store/9j02mfzk6b490g9i3jl03ghzh4ydbvsy-standard-library-1.5/src/Data/Maybe.agda:11,1-33
/nix/store/9j02mfzk6b490g9i3jl03ghzh4ydbvsy-standard-library-1.5/_build:
createDirectory: permission denied (Read-only file system)

(CLI agda My.agda runs fine, agda-mode-vscode as well.)

NixOS installs a wrapper (see nixpkgs/build-support/agda/default.nix) for Agda:

    makeWrapper ${Agda}/bin/agda $out/bin/agda \
      --add-flags "--with-compiler=${ghc}/bin/ghc" \
      --add-flags "--library-file=${library-file}" \
      --add-flags "--local-interfaces"

while ALS apparently calls Agda directly as a library.

One solution would be to allow user to supply flags to call Agda with (the crucial one here being --local-interfaces).

[banacorn]

Sorry for the late response.

One solution would be to allow user to supply flags to call Agda with (the crucial one here being --local-interfaces).

Yes, I think this is the way to go. This would also allow user to supply other flags they want to Agda.

[wldhx]

Are you going to implement this yourself, or would you like me to take a stab?

[banacorn]

That'd be great! I know how to get flags from agda-mode-vscode's settings to the language server (with LSP custom method and some stuff). But I don't know how to feed those flags to Agda. I think it can use some stabbing, if you're interested in this part.

[wldhx]

Upon looking, here's the place: src/Agda.hs#L51.

This patch seems to work for me:

diff --git a/src/Agda.hs b/src/Agda.hs
index 2c001e3..dc2bcdf 100644
--- a/src/Agda.hs
+++ b/src/Agda.hs
@@ -7,7 +7,7 @@ import Agda.Convert (fromResponse)
 import Agda.Interaction.Base (Command, Command' (Command, Done, Error), CommandM, CommandState (optionsOnReload), IOTCM, initCommandState)
 import qualified Agda.Interaction.Imports as Imp
 import Agda.Interaction.InteractionTop (initialiseCommandQueue, maybeAbort, runInteraction)
-import Agda.Interaction.Options (CommandLineOptions (optAbsoluteIncludePaths))
+import Agda.Interaction.Options (CommandLineOptions (optAbsoluteIncludePaths, optLocalInterfaces))
 import Agda.TypeChecking.Errors (prettyError, prettyTCWarnings')
 import Agda.TypeChecking.Monad
   ( TCErr,
@@ -48,7 +48,7 @@ interact = do

     -- start the loop
     opts <- commandLineOptions
-    let commandState = (initCommandState commands) {optionsOnReload = opts {optAbsoluteIncludePaths = []}}
+    let commandState = (initCommandState commands) {optionsOnReload = opts {optAbsoluteIncludePaths = [], optLocalInterfaces=True}}

     _ <- mapReaderT (`runStateT` commandState) (loop env)

Work needs to be done to make these user-specifiable.

[banacorn]

Wow is that all it takes?

[banacorn]

Now it's possible to supply flags to Agda like this:

als +AGDA --cubical -AGDA

Or though the settings of agda-mode