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

Question

我正在尝试为Agda设置一个ArchLinux虚拟机。到目前为止，我已经安装了所需的依赖项和Agda本身，但是当我试图编译一个用Agda编写的简单Hello程序时，我得到了一个Haskell错误。下面是场景描述。

虚拟机已被安排使用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应用程序，以查看一切是否顺利。愚蠢的应用程序如下：

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) )
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

我试图使用阴谋来安装ieee754，但是它说这个包已经安装好了。

你知道我怎么才能摆脱它吗？我是不是遗漏了什么？

这里 --它是包含虚拟机的GitHub回购。为了重现问题，只需遵循存储库的自述文件中所描述的内容就足够了。

Answer 1

正如本期在Agda GitHub页面上所建议的那样，这似乎是一个与Agda版本2.5.3相关的问题。

为了解决这个问题，我用stack代替了stack。我是说：

pacman --noconfirm -Sy stack

然后，在配置执行之后，我遵循了GitHub注释建议，它说：

只需告诉堆栈安装这些软件包：stack exec --package ieee754 --package text agda。之后的执行可以只使用堆栈执行agda。

这样，我就能够安装两个缺少的软件包，以便进行适当的MAlonzo编译。