Agda:使用Stack进行安装时找不到std-lib [英] Agda: Can't find std-lib when installing with Stack

问题描述

我正在尝试编译一个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在哪里寻找标准库?这是因为堆栈问题吗?

如果使用Ubuntu 17.10，那会有所帮助.

解决方案

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

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

I'm trying to compile an Agda file, but I'm having trouble getting it to find the standard library. I've seen the documentation here.

I've used Stack to install it:

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

And I've set the environment variable for my Agda directory:

> echo $AGDA_DIR
/home/joey/.agda

Which is populated with the correct files:

/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

However, when I go to compile an Agda file, I get the following error:

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

How can I tell Agda where to look for the standard library? Is this a problem because of Stack?

I'm on Ubuntu 17.10, if that makes a difference.

解决方案

It turns out that if you have a .agda-lib file in your root directory, it will completely ignore the defaults file. So the key was to include standard-library explicitly in that file.

A dumb thing for me to miss, but hopefully others with the same problem will find this answer.

这篇关于Agda:使用Stack进行安装时找不到std-lib的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！