我安装了一个 Agda 编译器，二进制文件可以来自这里:http://ocvs.cfv.jp/Agda/how-to-install-windows.html
...我正试图让它编译一个简单的 hello world 应用程序(我在网上找到了 Agda 'Hello World' 代码)
但我之前从未使用过 Emacs，不知道从哪里开始，也不知道使用哪些命令来编译和运行。我是 Agda 的新手，它似乎对编译器的选择有限，并且缺乏任何分步教程。下面是带有我找到的代码的 Emacs 编译器的屏幕截图:
open import System.IO using ( _>>_ ; putStr ; commit )
module System.IO.Examples.HelloWorld where
main = putStr "Hello, World\n" >> commit
我正在寻找运行简单的“Hello World”程序的分步说明
另一个编译器的工作示例也是可以接受的答案
谢谢!
最佳答案
看起来您尝试过类似一般的操作 M-x compile而不是任何特定的 Agda 功能。Agda:run Emacs 模式行中的模式指示器表明您在另一个缓冲区中有一个正在运行的 Agda 进程，但您并没有查看它。 Agda 模式可能有类似 agda-eval-buffer 的内容这应该将您当前的程序传递给该进程，并在 Pane 的下半部分显示结果。 (如果您以某种方式无法通过其他方式到达该缓冲区，请尝试手动切换到名为 *inferior-agda* 之类的缓冲区。)
您链接到的站点说它是 Agda 1，您实际上应该在不同的站点上寻找 Agda 2。
线下是我的原始答案，它可能仍然提供一些有用的见解。
错误信息表明您需要安装 make .
我猜在你修复这个依赖项后可能还有其他缺失的依赖项。理想情况下，文档应明确指定您需要安装的内容。make只是一个包装器，用于运行在本地 Makefile 中找到的任何命令。 .如果没有这样的文件，您可能希望将编译命令更改为其他内容。 (通常 Emacs 会要求你输入一个命令来运行，但提供了一个合理的默认值。)
关于emacs - 在 Agda emacs 中运行 'Hello World' 应用程序，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/50901672/