如何运行编译生成的Agda .agdai二进制文件？

关键说明 #

.agdai并非可执行文件，它是Agda生成的接口文件，用于存储模块的类型检查信息，供其他依赖模块编译时复用，本身不具备可执行性，所以双击无反应是正常的。

正确生成并运行可执行文件的步骤 #

假设你的源文件名为HelloWorld.agda：

1. 生成可执行文件
   在终端执行编译命令：

   agda --compile HelloWorld.agda
   

   执行完成后，当前目录会生成与源文件同名的可执行程序（Linux/macOS下为HelloWorld，Windows下为HelloWorld.exe）。
2. 运行程序
   • Linux/macOS环境：

     ./HelloWorld
     

   • Windows环境：

     HelloWorld.exe
     

额外提示 #

只有当你的代码中包含main IO函数时，上述编译命令才会生成可执行文件。如果是纯类型验证的模块，.agdai就是正常的编译产物，无需运行。

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