Open VladimirMarko opened 7 months ago
On the other end of the complexity spectrum, I have this error on stock Ubuntu 23.10, loading the language server through VSCode (1.87.0) and this extension.
The steps I took:
The only difference I'm seeing is restarting does not give me a different error. I can reproduce this every time I open VSCode and C-c C-l
in an Agda file.
Edit: I also seem to be experiencing #139
I believe the NixOS issue is happening because als
has dynamic library dependencies which likely aren't satisfied due to the NixOS environment. You'll probably need to figure out how to install als
manually so it's built to work under NixOS. I haven't managed to find a derivation for it yet though...
The alternative is to use something like nix-ld to add the dependencies to your environment, but I couldn't get this to work cause VSCode/agda-mode-vscode (not sure which) doesn't seem to be respecting the environment variables I've set before launching VSCode. My temporary workaround is to launch the downloaded (unpatched) als
inside the following flake's devshell:
{
description = "agda-env";
inputs = {
nixpkgs.url = "nixpkgs/nixpkgs-unstable";
utils.url = "github:numtide/flake-utils";
};
outputs = { self, nixpkgs, utils }: utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs { inherit system; };
inherit (pkgs) agda gmp icu70 lib libz mkShell ncurses stdenv vscode;
in
{
devShells.default = mkShell {
packages = [ agda vscode ];
NIX_LD_LIBRARY_PATH = lib.makeLibraryPath [
gmp
icu70
libz
ncurses
];
NIX_LD = builtins.readFile "${stdenv.cc}/nix-support/dynamic-linker";
};
});
}
...by running:
Agda_datadir=$HOME/.config/Code/User/globalStorage/banacorn.agda-mode/v0.2.6.4.0.3-linux/data/ $HOME/.config/Code/User/globalStorage/banacorn.agda-mode/v0.2.6.4.0.3-linux/als -p
(You may need to adjust some paths.)
Edit: after using this some more, I'm having trouble with imports, and I haven't figured out why yet. So even this workaround doesn't appear to be a complete solution.
You can instead try to install the standard library manually as described here, which should work.
I am on Windows 10 and I want to write some Agda code.
The HoTT Game recommends that I install NixOS on WSL2 and run Agda there.
So I installed NioOS using
wsl --import NixOS .\NixOS\ nixos-wsl.tar.gz --version 2
as described in NixOS-WSL.Now, the current version of NixOS-WSL does not support VS Code out of the box (issue here), so I used this flake to fix that, as recommended in the issue.
That means that my current configuration is as follows: NixOS in WSL2 on Windows 10 with
/etc/nixos/
containing:flake.nix
:configuration.nix
:NixOS-WSL specific options are documented on the NixOS-WSL repository:
https://github.com/nix-community/NixOS-WSL
{ config, lib, pkgs, ... }:
{ imports = [ ];
wsl.enable = true; wsl.defaultUser = "nixos";
nix.settings.experimental-features = [ "nix-command" "flakes" ];
This value determines the NixOS release from which the default
settings for stateful data, like file locations and database versions
on your system were taken. It's perfectly fine and recommended to leave
this value at the release version of the first install of this system.
Before changing this value read the documentation for this option
(e.g. man configuration.nix or on https://nixos.org/nixos/options.html).
system.stateVersion = "23.11"; # Did you read the comment? }
AgdaTest.agda
with some Agda code.Now, in this folder (
~/agda-test
) I run:nix develop
code .
This opens the folder in VS Code in Windows, as intended.
I open
AgdaTest.agda
in this VS Code instance, goC-c C-l
and it fails.I initially got this error:
I tried doing
chmod a+x als
, but this had no effect - the error persisted as it was despite the added permission, and I subsequently reversed that change.Now, writing this issue, I restarted everything and seemingly spontaneously got a different error after
C-c C-l
: