<div dir="ltr">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.<div><br></div><div>$ time ./Hello</div><div>Hello World</div><div>user<span class=""> </span>0m0.002s</div><div><br></div><div>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.</div><div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 10, 2015 at 12:08 AM, Peter Hancock <span dir="ltr"><<a href="mailto:hancock@fastmail.fm" target="_blank">hancock@fastmail.fm</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 09/12/2015 18:23, Ulf Norell wrote:<br>
<br>
> $ time agda -c Hello.agda -i. -iagda-prelude/src<br>
> --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs<br>
> [...]<br>
> Linking /Users/ulfn/research/scratch/tmp/Hello ...<br>
> user 0m7.155s<br>
<br>
</span>Wow! Is that the build time? 7 milliseconds?<br>
<br>
> $ ./Hello<br>
> Hello World<br>
<br>
To within a small power of 10, in how many milliseconds<br>
after pressing CR did the 'H' appear?<br>
<br>
Sceptically,<br>
<br>
Hank<br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>