[Agda] compiling Hello.agda

[Serge D. Mechveliani]

On Wed, Jul 18, 2012 at 08:48:11PM +0200, Paul van der Walt wrote:
> Hi Serge,
> 
> On Wed, Jul 18, 2012 at 22:11:58 +0400, quoth Serge D. Mechveliani:
> > I put this file to  $myProjectRoot  and command there
> > (in Debian Linux, tcshell)
> > 
> >  agda -c -i /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1 Hello.agda
> 
> This all looks good, but I think you should also add "-i ." to
> you command - Agda must also search the current directory to be
> able to find your module.


Thanks to people,
I managed to compile and run  Hello.agda
(see my first letter on this subject).

But this was in a bit strange way. There remain questions.

The command is  
               agda -c -i . -i $agdaLibSrc Hello.agda

where  $agdaLibSrc = /home/mechvel/haskell/agda/lib-0.6/src
-- the place where the Standard Library source resides.

1. This looks strange, because it is natural for the compiler to take 
   lib from the  .a  files, and the .a files are installed in 
   $agdaLib = /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1
First, I tried  -i $agdaLib,  and the compiler reported that it does not
find  Data.String ...  Indeed,   $agdaLib/  does not contain this module.
Then, I try  -i $agdaLibSrc,  and it compiles -- with revealing the 
following strange features.

2. For my program
--------------------------
module Hello where
data Unit : Set where
 unit : Unit
{-# COMPILED_DATA Unit () () #-}
postulate IO : Set -> Set 
{-# COMPILED_TYPE IO IO #-}

open import Data.String 
postulate
  putStrLn : String -> IO Unit
{-# COMPILED putStrLn putStrLn #-}
main : IO Unit
main = putStrLn "hello!" 
---------------------------

(taken from  tutorial.pdf)
the compiler reports an error, and insists on setting 
                                   {-# BUILTIN IO IO #-}             
rather than                        {-# COMPILED_TYPE IO IO #-}
So, I just insert  {-# BUILTIN IO IO #-}
after the line of  {-# COMPILED_TYPE IO IO #-}.

What do you think of this, please?

3. Then,       agda -c -i . -i $agdaLibSrc Hello.agda

proceeds with about  30 minute  compilation:
-------------
...
Skipping Data.Sum (/home/mechvel/haskell/agda/lib-0.6/src/Data/Sum.agdai).
Skipping Data.Product 
      (/home/mechvel/haskell/agda/lib-0.6/src/Data/Product.agdai)
[many `Skipping']
...
Compiling Algebra.Operations in 
/home/mechvel/haskell/agda/lib-0.6/src/Algebra/Operations.agdai to 
/home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/Algebra/Operations.hs
...
[many `Compiling']
-------------

So, it compiles the `program' Operations.agdai  from the library _sources_
to an  .hs  program, with creating a directory in my project root.
And what is  .agdai  -- the interface module, or maybe, `interpreted'?

Then, it applies  ghc:
--------
calling: ghc -O -o /home/mechvel/haskell/agda/myPrograms/Hello 
           -i/home/mechvel/haskell/agda/myPrograms -main-is MAlonzo.Code.Hello 
           /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/Hello.hs 
           --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns 
           -Werror
[ 1 of 88] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
...
[88 of 88] Compiling MAlonzo.Code.Hello 
  ( /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/Hello.hs, 
   /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/Hello.o )
Linking /home/mechvel/haskell/agda/myPrograms/Hello ...
--------

Then,  ./Hello  works.

Really, must it need 30 minutes and  90% of 512 Mb memory to build the  
"hello!"  program?

4. Then, I remove  Hello, Hello.agdai,  and repeat

   agda -c -i . -i $agdaLibSrc Hello.agda            

Now, it builds in 30 seconds. This is faster, probably, because it 
reuses the modules prepared by the previous attempt in  ./MAlonzo/ 
Now, if I add some `import' to my program, will Agda run into a long 
compilation of some more modules from  Standard library ?
There is something strange about all this,
because the Standard library has already been compiled to  .a  and 
installed to  
  $agdaLib = /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1

Can you comment, please?


5. I try a module which does not use any library:

  module AgdaBasics where
  data Bool : Set where
   true  : Bool
   false : Bool

 agda -c -i . -i $agdaLibSrc AgdaBasics.agda

yields 

Skipping AgdaBasics (/home/mechvel/haskell/agda/myPrograms/AgdaBasics.agdai).
Compiling AgdaBasics in 
  /home/mechvel/haskell/agda/myPrograms/AgdaBasics.agdai to 
  /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/AgdaBasics.hs
calling: ghc -O -o /home/mechvel/haskell/agda/myPrograms/AgdaBasics 
 -i/home/mechvel/haskell/agda/myPrograms -main-is MAlonzo.Code.AgdaBasics 
  /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/AgdaBasics.hs 
  ...
[1 of 2] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[2 of 2] Compiling MAlonzo.Code.AgdaBasics 
 ( /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/AgdaBasics.hs,
  /home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/AgdaBasics.o )

Compilation error:
/home/mechvel/haskell/agda/myPrograms/MAlonzo/Code/AgdaBasics.hs:1:1:
    The function `main' is not defined in module `MAlonzo.Code.AgdaBasics'
--------------

Agda  treating of `main' differs from GHC one. Agda insists on that there
must be `main' and that compiling must necessarily be accomplished with
building an executable -- ?
What may be the simplest possible dummy `main' ?


6. I have seen the pragma like `ExistentialTypes' somewhere in the 
   Agda Standard library  source.
Does this mean that Agda compiles at the initial stage the  .agda  code 
to the Haskell-GHC code that relies on ExistentialTypes ?

As I recall, the GHC people tried to express dependent types via the
ExistentialTypes in the Haskell-GHC extension. The code was too complex
to write an application by hand. Also I could not understand whether 
ExistentialTypes worked, and even how must they work.
I wrote (about 12 years ago): 
"Let anyone write some small prototype algebra library in 
Haskell+GHC+ExistentialTypes, so that the code will look reasonably, and 
will work, and we shall see".
And nobody wrote.

Now, is Agda trying to generate the above code for 
Haskell+ExistentialTypes  automatically?

Thank you in advance for help,

------
Sergei
mechvel at botik.ru