Bug#992448: agda: fails to compile hello world

Francis Southern francis.southern at gmail.com
Wed Aug 18 20:03:45 BST 2021


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



More information about the Pkg-haskell-maintainers mailing list