在Agda emacs中运行"Hello World"应用程序

Question

我安装了一个Agda编译器,binarys可以从这里: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'程序

使用另一个编译器的工作示例也是可接受的答案

谢谢!

Answer 1

看起来您尝试了一般性的功能，M-x compile而不是任何特定的 Agda 功能。

Emacs 模式行中的模式指示器Agda:run表明您在另一个缓冲区中有一个正在运行的 Agda 进程，但您没有查看它。Agda 模式可能具有类似的功能agda-eval-buffer，可以将当前程序传递给该进程，并在窗格的下半部分显示结果。*inferior-agda*（如果您无法通过其他方式到达该缓冲区，请尝试切换到名为“手动”的缓冲区。）

您链接到的网站显示它是 Agda 1，您实际上可能应该在其他网站上查找 Agda 2。

下面是我原来的答案，它仍然可以提供一些有用的见解。

错误消息表明您需要安装make.

我猜修复此依赖项后可能还会缺少其他依赖项。理想情况下，文档应明确指定您需要安装的内容。

make只是一个包装器，用于运行在本地找到的任何命令Makefile。如果没有这样的文件，您可能需要将编译命令更改为其他命令。（通常 Emacs 会要求您输入要运行的命令，但会提供一个合理的默认值。）