[Agda] how to run helloworld in agda

[Sergei Meshveliani]

On Wed, 2015-12-09 at 17:35 +0000, Peter Hancock 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. 


I do this (under Debian Linux) this way.
  
  > agda -c -i /home/mechvel/agda/stLib/oct29-2015/src  Hello.agda

This prepares the executable  Hello  in  5 seconds  on a 3 GHz machine.
This includes 
1) type checking, 
2) compiling to the .hs file for Glasgow Haskell 
   (by appying MAlonzo, I guess)
3) applying Glasgow Haskell to compile from Haskell to the .o file and  
   linking the executable.

This does not include type-checking nor compiling of all necessary
Standard library modules. This has been done earlier, this can be
considered as a part of Standard library installation.

The sizes are: 

   Hello.agdai      --      6209 bytes,
   Hello executable -- 6.897.671 bytes.

The executable is large because there are linked many library functions,
mainly, for the string output to an output device.

------
Sergei