在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会要求您运行命令，但提供合理的默认值。）

Answer 2

鉴于我在Linux上运行并且不是agda专家，这个解决方案可能不值得。但我仍然会尝试一下。

当我在我的系统上安装agda和agda-stdlib时，它在agda2.el中为我提供了一个名为/usr/share/agda/emacs-mode的文件。那说我在~/.emacs.d/init.el文件中只有以下内容：

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

因为，你已经在Emacs中设置了agada模式，除非你的agda模式版本旧，否则以上版本不会有用。

我们可以使用M-x agda2-compile编译您在Emacs中打开的当前文件。这样做会打开另一个提示，要求你提供Backend。我使用GHC作为输入并编译它。是的，我遇到了一些我不知道如何解决的错误。所以，我在搜索引擎上查询并提出：

module memo where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Foreign.Haskell using (Unit)

main : IO Unit
main = putStrLn (toCostring "Hello, Agda!")

我需要指出，第一行module memo where应该与文件名相同，对于你的情况是memo.agda。

Answer 3

我现在在我的机器上运行了一个hello world程序。

以下代码编译和工作

open import Common.IO


main = putStrLn "Hello, world, strings working!"

是代码，存储在'hello.agda'文件中，我在emacs中编译为'hello'。我通过选择agda > compile来编译emacs，这是在正确安装agda时emacs上可用的选项。

我不能像朋友那样给我一个关于如何在emacs上安装agda的详细教程，但上面的代码可以工作，并在linux上编译emacs，这对我来说是设置的。