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

【问题标题】：INTERNAL ERROR when installing local package安装本地包时出现内部错误
【发布时间】：2021-05-29 00:36:04
【问题描述】：

我来了

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

【问题讨论】：

【解决方案1】：

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

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

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

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

【讨论】：