[Agda] how to run helloworld in agda

[John Leo]

Yes, sorry, I meant to compile and run, not to write.

It took a minute or more to compile on a top end Macbook Pro.  Typechecking
and compiling the standard library took the most time.  The executable is a
mere 12323368 bytes on my machine.

John

On Wed, Dec 9, 2015 at 9:35 AM, Peter Hancock <hancock at fastmail.fm> wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151209/87022c3b/attachment-0001.html