Agda:在用Stack安装时找不到std

Question

我试图编译一个Agda文件，但是我很难让它找到标准库。我看过文档这里。

我用Stack安装了它：

> which agda
/home/joey/.local/bin/agda

我已经为我的Agda目录设置了环境变量：

> echo $AGDA_DIR
/home/joey/.agda

它使用正确的文件填充：

/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/libraries
/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/defaults
standard-library

> cat /home/joey/agda/agda-stdlib/standard-library.agda-lib
name: standard-library
include: src

然而，当我去编译一个Agda文件时，我会得到以下错误：

Failed to find source of module Function in any of the following
locations:
  /home/joey/agda/AutoInAgda/src/Function.agda
  /home/joey/agda/AutoInAgda/src/Function.lagda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.agda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.lagda
when scope checking the declaration
  open import Function

我如何告诉Agda去哪里寻找标准库？这是因为Stack的问题吗？

我上的是Ubuntu 17.10，如果这有什么区别的话。

Answer 1

结果是，如果根目录中有一个..agda lib文件，它将完全忽略默认文件。因此，关键是在该文件中显式地包含standard-library。

对我来说，这是一件愚蠢的事情，但希望其他有同样问题的人能找到这个答案。