使用 Agda 编译的问题答案

【问题标题】：Problems compiling with Agda使用 Agda 编译的问题
【发布时间】：2019-09-05 00:10:49
【问题描述】：

我使用“apt-get install agda-mode”安装了 Adga。我有一个用 Agda 编写的“Hello World”程序，如下面的截图所示

但是当我转到 Agda > Compile 时，它会要求我提供第二个屏幕截图中显示的“后端”

我尝试输入“GHC”作为后端，但它只是说“/usr/share/libghc-agda-dev/MAlonzo/src: getDirectoryContents:openDirStream: 不存在（没有这样的文件或目录） '

Agda > 加载似乎有效。如何让我的 Agda 程序编译？

【问题讨论】：

【解决方案1】：

我个人建议你通过haskell的Cabal安装agda（你可以通过安装haskell-platform来获得它，安装haskell会安装ghc）。由 debian 维护的 agda 包目前已损坏，并且与标准库存在问题。

cabal update
cabal install agda

您可以通过apt install 安装标准库和agda-mode。毕竟（请记住，cabal 会编译 agda，因此需要一些时间），将标准库添加到 agda 的本地设置中。打开 emacs 并加载文件以对其进行类型检查，或者如果它具有可执行代码，则对其进行编译。

【讨论】：