[Agda] how to run helloworld in agda

[Mandy Martino]

Hi,
how to  find  the  path  of  stdlib after it  install ?
martin at ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs import Distribution.Simple
main = defaultMain
martin at ubuntu:~/adga2/stdlib/agda-stdlib$ lsagda-stdlib.agda-lib  GenerateEverything.hs  LICENCE              README.mdAllNonAsciiChars.hs   GNUmakefile            notes                Setup.hsCHANGELOG             Header                 publish-listings.sh  srcdoc                   index.sh               READMEffi                   lib.cabal              README.agda

Regards,
Martin 

> Subject: Re: [Agda] how to run helloworld in agda
> From: mechvel at botik.ru
> To: tesleft at hotmail.com
> CC: agda at lists.chalmers.se
> Date: Tue, 8 Dec 2015 21:06:16 +0400
> 
> On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:
> > The interactive mode is no longer supported. Don't complain if it
> > doesn't work.
> > Main> :l ag.agda
> > Checking ag (/home/martin/adga2/ag.agda).
> > /home/martin/adga2/ag.agda:3,13-25
> > Failed to find source of module IO.Primitive in any of the
> > following locations:
> > /home/martin/adga2/IO/Primitive.agda
> > /home/martin/adga2/IO/Primitive.lagda
> > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda
> > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda
> > when scope checking the declaration
> > open import IO.Primitive using (IO; putStrLn)
> > Failed.
> > Main>
> > 
> > module ag where
> > 
> > open import IO.Primitive using (IO; putStrLn)
> > open import Data.String using (toCostring; String)
> > open import Foreign.Haskell using (Unit)
> > 
> > main : IO Unit
> > main = putStrLn (toCostring "Hello, Agda!")
> > 
> 
> I remove  "module ag where"  (because this module has `main' in it),
> and apply
> 
>     agda -c $agdaLibOpt Hello.agda
> 
> where  $agdaLibOpt  contains the path to the  /src  directory of
> Standard library.
> This makes the executable file  Hello.
> Then, the command  
> 
>        ./Hello  
> prints  
> "Hello, Agda!"
> 
> 
> > why use open import, but not import
> 
> After  "import Foo",
> 
> one can write  Foo.foo,  if  foo  is defined in  Foo  module.
> After
>   import Foo
>   open Foo using (foo) 
> 
> one can write `foo' in the scope.
> And the line
> 
>   open import Foo using (foo)
> 
> combines the above lines of `import' and `open'.
> 
> Regards,
> 
> ------
> Sergei
> 
> 
> 
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151209/e28b5ebf/attachment.html