builddir 和 outputdir 是什么，为什么它们会生成“未找到文件”错误？

Question

目标：在 Idris2 中打包一个可执行的“Hello, world”程序

我在 docs 工作，它提供了包字段的描述，但遗憾的是没有提供任何示例。

问题：builddir 和 outputdir 上的“找不到文件”编译错误

以下是我的目录结构和内容的演练。

$ ls
kata.ipkg  README.md  src

$ ls src/
Index.idr

$ cat src/Index.idr 
module Index
main : IO ()
main = putStrLn "Hello, world"

$ cat kata.ipkg 
package kata
authors = "eleanorofs"
builddir = "build"
bugtracker = "https://gitlab.com/eleanorofs/idris-kata/-/issues"
executable = "src/Index.idr"
outputdir = "dist"
homepage = "https://gitlab.com/eleanorofs/idris-kata"
main = Index
maintainers = "eleanorofs"
opts = "--cg node --directive pretty"
readme = "./README.md"
sourcedir = "./src"
sourceloc = "https://gitlab.com/eleanorofs/idris-kata"
version = 0.0.1

$ idris2 --build kata.ipkg
1/1: Building Index (./src/Index.idr)
Uncaught error: File error (dist/src/Index.idr): File Not Found

当我删除

outputdir

行时，它给了我同样的错误，但是在

builddir

（build/exec/src/Index.idr代替。

问题

这让我觉得我误解了一些关于这个编译器应该如何工作的非常基本的东西。

1. Idris 自己维护着build/ 和dist/ 的内容，对吧？所以我不需要对这些目录做任何事情，对吧？

2. 如果是这样，为什么它成功构建了 Index.idr 但随后在尝试查找我期望它自己生成的文件时出现错误？