Running a 'Hello World' app in Agda emacs

Question

I installed an Agda compiler, binarys can be from here: http://ocvs.cfv.jp/Agda/how-to-install-windows.html

... and I'm trying to make it compile a simple hello world app (I found the Agda 'Hello World' code online)

But I've never used Emacs before, and I don't know where to begin, or which commands to use to compile and run. I'm new to Agda, which seems to have limited options for compilers, and is lacking any step by step tutorial. Below is a screenshot of the Emacs compiler with the code I found:

open import System.IO using ( _>>_ ; putStr ; commit )

module System.IO.Examples.HelloWorld where

main = putStr "Hello, World\n" >> commit

I'm looking for step by step instructions to run a simple 'Hello World' program

A working example with another compiler would also be an acceptable answer

Thanks!

Recourse

Have you read the docs? – Orison

I have now, but I need a basic step by step guide – Recourse

Please edit your question to include the error message as text so that we can copy/paste it and so that Google can find it. – Testimony

Also piease reveal what exactly you did to produce this error message. Did you type a command like M-x compile or did you use some keystroke sequence like C-c C-c? – Testimony

Answer 1

This looks like you attempted something like the general M-x compile rather than any specific Agda functionality.

The Agda:run mode indicator in the Emacs mode line suggests that you have a running Agda process in another buffer, but you're not looking at it. The Agda mode probably has something like agda-eval-buffer which should pass your current program to that process, and bring up the results in the lower half of the pane. (Try switching to a buffer called something like *inferior-agda* manually if you somehow cannot reach that buffer by other means.)

The site you link to says it's Agda 1 and you should probably actually look for Agda 2 on a different site.

Below the line is my original answer, which may still provide some useful insight.

---

The error message indicates that you need to install make.

I'm guessing there may be additional missing dependencies after you fix this one. Ideally the documentation should explicitly specify exactly what you need to install.

make is just a wrapper to run whatever cormands are found in the local Makefile. If there is no such file, you will probably want to change the compilation command to something else. (Typically Emacs asks you for a command to run, but supplies a plausible default.)

Testimony

Answer 2

Given I am running on Linux and am no agda expert, this solution might not be worth it. But still I will give it a try.

When I installed agda and agda-stdlib on my system, it provides me with a file called agda2.el in /usr/share/agda/emacs-mode. That said I just had the following in my ~/.emacs.d/init.el file:

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

Since, you already have agada mode setup in Emacs the above wont be useful unless your version of agda mode is old.

We can compile the current file you have opened in Emacs using M-x agda2-compile. Doing this will open up another prompt asking you for a Backend. I used GHC as input and it compiled it. Yes, and I got some errors I don't know how to fix. So, I queried on a search engine and came up with:

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!")

I need to point out that the first line module memo where should be same as the filename which for your case is memo.agda.

Mckeever

Answer 3

I now have a hello world program running on my machiene.

The following code compiles and works

open import Common.IO


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

is the code, stored in the file 'hello.agda', which I compile in emacs to 'hello'. I compile in emacs by selecting agda > compile, an option that is available on emacs when agda is installed correctly.

I can't give a detailed tutorial as to how to install agda on emacs as a friend did it for me, but the above code works, and compiles on emacs on linux, which is the set up which is working for me.

Recourse