Agda项目编译生成的src/MAlonzo目录是否需要添加到.gitignore？

是否需要提交src/MAlonzo到版本库 #

不需要。该目录下的所有.hs、.o等文件都是Agda编译过程中生成的中间构建产物，完全可以通过重新编译你的Agda源码完整复现，没有任何需要纳入版本控制的自定义内容。

通常是否会将/src/MAlonzo加入.gitignore #

是，这是Agda开发者的通用实践。自动生成的构建产物不需要纳入版本追踪，加入忽略规则后可以避免误提交大量无关文件，也不会干扰本地代码变更的对比检查。

为什么构建产物默认生成在src目录而非_build目录 #

这是Agda MAlonzo编译后端的默认设计选择：

• 早期设计时优先考虑调试便利性，生成的Haskell中间代码放在源码目录下，开发者可以更快速地定位和查看生成的中间代码
• 避免预设构建目录结构，减少适配不同项目自定义目录规则的复杂度

如果需要调整输出目录，可以在编译时添加--compile-dir参数手动指定，例如要输出到_build目录，使用如下编译命令即可：
agda --compile --compile-dir=_build src/MyProject/Main.agda

内容的提问来源于stack exchange，提问作者Jo Liss