我正在尝试编译一个Agda文件,但是我很难让它找到标准库。我看过文档here

我已经使用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在哪里寻找标准库?这是因为堆栈问题吗?

我使用Ubuntu 17.10,如果有帮助的话。

最佳答案

事实证明,如果您的根目录中有一个.agda-lib文件,它将完全忽略默认文件。因此关键是要在该文件中明确包含standard-library

我想念一个愚蠢的东西,但希望其他有相同问题的人会找到这个答案。

10-08 12:35