[Agda] how to run helloworld in agda

[Peter Hancock]

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