Idris2打包Hello World时builddir与outputdir报文件未找到错误

问题根源与解决方案 #

你的核心问题是kata.ipkg里的executable字段配置错误——这个字段应该填写输出的可执行文件名称，而不是源文件路径。修正后即可解决文件找不到的错误。

修正后的kata.ipkg内容：

package kata
authors = "eleanorofs"
builddir = "build"
bugtracker = "https://gitlab.com/eleanorofs/idris-kata/-/issues"
executable = "kata"  # 修改为可执行文件名，而非源文件路径
outputdir = "dist"
homepage = "https://gitlab.com/eleanorofs/idris-kata"
main = Index  # 正确：指定包含main函数的模块名
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

编译完成后，Idris会自动创建build（存放中间编译文件）和dist（存放最终可执行文件）目录，你可以在dist下找到生成的可执行文件kata。

解答你的疑问 #

1. build/和dist/目录是否由Idris自行维护？
   是的，这两个目录完全由Idris自动管理，编译时会自动创建，无需手动创建或修改其中的内容。builddir用于存放编译过程中的临时中间文件，outputdir用于存放最终生成的可执行文件或库文件。

2. 为何成功编译Index.idr后，却找不到本该由编译器生成的文件？
   因为你错误地将executable字段设为源文件路径src/Index.idr，Idris误以为你要将可执行文件输出到该路径下，进而尝试在outputdir（或默认的build目录）下寻找这个不存在的路径，最终触发File Not Found错误。修正executable字段为纯文件名后，编译器就能正确生成并定位文件了。

内容的提问来源于stack exchange，提问作者Eleanor Holley