Source: agda Version: 2.5.4.1-3 Severity: important Dear Maintainer,
*** Reporter, please consider answering these questions, where appropriate *** * What led up to the situation? * What exactly did you do (or not do) that was effective (or ineffective)? * What was the outcome of this action? * What outcome did you expect instead? *** End of the template - remove these template lines *** I installed the following packages: agda/stable 2.5.4.1-3 all agda-bin/stable 2.5.4.1-3+b1 amd64 agda-mode/stable 2.5.4.1-3 all agda-stdlib/stable,now 0.17-1 all agda-stdlib-doc/stable 0.17-1 all I followed the instructions at <https://agda.readthedocs.io/en/v2.6.2/getting-started/hello-world.html>. The file <hello.agda> checked correctly within Emacs, but when I tried to compile the file <hello-world.agda> I received the following output: $ agda --compile hello-world.agda Compiling Agda.Primitive in /usr/share/libghc-agda-dev/lib/prim/Agda/Primitive.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Primitive.hs Compiling Agda.Builtin.Unit in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Unit.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/Unit.hs Compiling Agda.Builtin.IO in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/IO.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/IO.hs Compiling Agda.Builtin.Bool in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Bool.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/Bool.hs Compiling Agda.Builtin.Nat in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Nat.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/Nat.hs Compiling Agda.Builtin.Char in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Char.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/Char.hs Compiling Agda.Builtin.List in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/List.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/List.hs Compiling Agda.Builtin.String in /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/String.agdai to /home/$user/code/agda/MAlonzo/Code/Agda/Builtin/String.hs Compiling hello-world in /home/$user/code/agda/hello-world.agdai to /home/$user/code/agda/MAlonzo/Code/QhelloZ45Zworld.hs agda: /usr/share/libghc-agda-dev/MAlonzo/src: getDirectoryContents:openDirStream: does not exist (No such file or directory) A brief web search led me to believe that this was a problem with the Debian package and I uninstalled the packages listed above and installed Agda with cabal instead, which produces the expected output. -- System Information: Debian Release: 10.10 APT prefers stable-updates APT policy: (500, 'stable-updates'), (500, 'stable') Architecture: amd64 (x86_64) Kernel: Linux 4.19.0-16-amd64 (SMP w/2 CPU cores) Locale: LANG=en_GB.UTF-8, LC_CTYPE=en_GB.UTF-8 (charmap=UTF-8), LANGUAGE=en_GB:en (charmap=UTF-8) Shell: /bin/sh linked to /usr/bin/dash Init: systemd (via /run/systemd/system) LSM: AppArmor: enabled