[Agda] how to run helloworld in agda

[Ulf Norell]

7 seconds to build the Prelude and its dependencies (23 modules and 1500
loc) from scratch. 4 seconds of those are spent running the Haskell
compiler. Once that's done, changing Hello.agda and rebuilding takes 0.8s.

$ time ./Hello
Hello World
user 0m0.002s

In my experience Agda is around a factor 2 slower than comparable Haskell
code. Of course, in Agda it's much easier to get carried away and write
code that performs poorly.

/ Ulf


On Thu, Dec 10, 2015 at 12:08 AM, Peter Hancock <hancock at fastmail.fm> wrote:

> On 09/12/2015 18:23, Ulf Norell wrote:
>
> > $ time agda -c Hello.agda -i. -iagda-prelude/src
> > --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs
> > [...]
> > Linking /Users/ulfn/research/scratch/tmp/Hello ...
> > user 0m7.155s
>
> Wow!  Is that the build time?  7 milliseconds?
>
> > $ ./Hello
> > Hello World
>
> To within a small power of 10, in how many milliseconds
> after pressing CR did the 'H' appear?
>
> Sceptically,
>
> Hank
>
> _______________________________________________
> 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/20151210/6b17d639/attachment.html