[Agda] how to run helloworld in agda

[Peter Hancock]

On 09/12/2015 17:05, John Leo wrote:

...

> So I had to add it and run ghc manually:
> 
> ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda
> -i/Users/leo/agda/agda-stdlib-0.11/ffi  -main-is MAlonzo.Code.Hello
> /Users/leo/agda/MAlonzo/Code/Hello.hs --make -fwarn-incomplete-patterns
> -fno-warn-overlapping-patterns

...

> I think Agda has to win the award as the serious language which requires
> the most work to write hello world.

ROFLMAO. Well, it was easy enough to write the program, the problem
was the JCL used to build an executable, and to invoke it. 

For very low motives, I am dying to know how long a runnable hello world takes to build,
and how large it is. 

Peter Hancock