Haskell编译器在编译修改后的Alonzo程序时失败

Question

我正在尝试为Agda设置ArchLinux虚拟机。到目前为止，我已经安装了必需的依赖项和Agda本身，但是当我尝试编译用Agda编写的简单Hello World程序时，出现了Haskell GHC错误。以下是方案说明。

已使用Vagrant安排了虚拟机。我的配置脚本执行以下软件包安装：

pacman --noconfirm -Syyu
pacman --noconfirm -Sy ansible vim nano unzip wget git make gcc clang dnsutils
yes | pacman -Sy virtualbox-guest-utils
pacman --noconfirm -Sy emacs
pacman --noconfirm -Sy ghc-static ghc-libs ghc
pacman --noconfirm -Sy cabal-install    
pacman --noconfirm -Sy agda
pacman --noconfirm -Sy agda-stdlib

该vagrant up过程完成后，我将进行SSH登录，然后尝试构建并启动一个简单的Agda helloworld应用程序，以查看一切是否正常。愚蠢的应用程序如下：

module helloworld where
open import IO

main = run (putStrLn "Hello World")

要使用Agda进行编译，我使用以下命令：

agda -i /usr/share/agda/lib/ -i . -c helloworld.agda

但是，当编译运行时，出现以下错误：

Calling: ghc -O -o /vagrant/helloworld -Werror -i/vagrant -main-is MAlonzo.Code.Qhelloworld /vagrant/MAlonzo/Code/Qhelloworld.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[ 1 of 78] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
Compilation error:

MAlonzo/RTE.hs:5:1: error:
    Could not find module ‘Numeric.IEEE’
    There are files missing in the ‘ieee754-0.8.0’ package,
    try running 'ghc-pkg check'.
    Use -v to see a list of the files searched for.
  |
5 | import Numeric.IEEE ( IEEE(identicalIEEE) )
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

我试图安装ieee754using cabal，但是它说软件包已经安装。

你知道我怎么摆脱它吗？我想念什么吗？

这是包含虚拟机的GitHub存储库。为了重现该问题，只需遵循存储库的自述文件中描述的内容。

Answer 1

正如在Agda GitHub页面上针对此问题的建议，似乎是与Agda版本2.5.3相关的问题。

为了解决我已经更换cabal-install与stack替代。我的意思是：

pacman --noconfirm -Sy stack

然后，在执行供应之后，我遵循了GitHub注释建议，说：

只需告诉堆栈安装以下软件包即可：stack exec --package ieee754 --package text agda。可以仅使用堆栈执行agda来执行此操作。

这样做，我能够安装两个缺少的软件包以进行正确的MAlonzo编译。