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

问题描述

我要了

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 没有帮助。

解决方法

显然是因为编译器还没有创建必要的目录（fix is pending）。可以通过手动创建目录并设置 $IDRIS2_PREFIX（$PREFIX 用于使用 make）来修复

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

我不明白为什么这意味着我可以在我的可执行文件中使用 foo 包（从文档中我认为我需要将它们放在 depends 目录中，或者 {{1} }) 但我可以。

据推测，这也意味着如果其他依赖项不在 export IDRIS2_PREFIX=$(pwd)/out 中，则无法访问它们。我这里只有一个依赖项，所以我没有尝试过。