安装本地包时出现内部错误

Question

我得到了

Uncaught error: INTERNAL ERROR: Can't make directory foo

当尝试安装我的本地库时。我在一个目录中运行idris2 --install foo.ipkg

.
+-foo.ipkg
+-src
  +-Util.idr

包含文件内容

package foo 
version = "0.0.1"

sourcedir = "src"
modules = Util

和

module Util

我一直在关注these docs，我想知道这是否与他们提到的写权限和$PREFIX有关。设置PREFIX=<some_dir> idris2 --install foo.ipkg没有帮助。

Answer 1

显然，这是因为编译器还没有创建必要的目录(fix is pending)。可以通过手动创建目录并设置$IDRIS2_PREFIX (使用make时使用$PREFIX)来修复此问题

mkdir -p out/idris2-0.3.0
IDRIS2_PREFIX=$(pwd)/out idris2 --install foo.ipkg 

我不明白为什么这意味着我可以在我的可执行文件中使用foo包(从文档中，我认为我需要将它们放在depends目录中，或者export IDRIS2_PREFIX=$(pwd)/out中)，但是我可以。

这可能还意味着，如果其他依赖项不在out/中，则它们将无法访问。我这里只有一个依赖项，所以我没有尝试过。