[Agda] compiling Hello.agda

Andreas Abel andreas.abel at ifi.lmu.de
Thu Jul 19 19:08:21 CEST 2012 

Here some quick answers:

1. 3. The standard library is not precompiled into an .a file (except 
the small ffi binding you mention).  So, it must be compiled from source 
to haskell at least once, and that takes very long.

2. The tutorial might not be completely up-to-date.  IO is a builtin, so 
you need the builtin-pragma.

4. Yes, it reuses the previously compiled .hs .hi and .o files.

5. Currently, the MAlonzo compiler requires a main routine.

6. MAlonzo seems to rely on the ExistentialTypes extension.  However, it 
does not translate dependent types into Haskell.  It produces almost 
untyped code, and casts everything with unsafeCoerce...

Cheers,
Andreas

On 19.07.2012 16:34, Serge D. Mechveliani wrote:
> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

More information about the Agda mailing list