[Agda] how to run helloworld in agda

[Mandy Martino]

after untar  https://agda.github.io/agda-stdlib
into  directory /home/martin/adga2/agda-stadlib
cd  fficabal install Setup.hs
does it mean that the  extracted  file path is the library  path ?
/home/martin/adga2/agda-stadlib ?

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: Wed, 9 Dec 2015 15:41:17 +0400
> 
> On Wed, 2015-12-09 at 19:11 +0800, Mandy Martino wrote:
> > Hi,
> > 
> > 
> > how to  find  the  path  of  stdlib after it  install ?
> > 
> 
> For example, I have installed Standard library in 
> 
>     /home/mechvel/agda/stLib/oct29-2015/src,
> 
> so that this directory contains Algebra.agda, and other .agda files and
> subdirectories.  
> Agda is called as 
> 
>   agda -c $agdaLibOpt MyProgram.agda
> 
> where  $agdaLibOpt  is
> 
>  -i . -i /home/mechvel/agda/stLib/oct29-2015/src -i /home/mechvel/source
> 
> It lists 3 paths. The last path points to where reside my .agda files
> which MyProgram imports. 
> 
> ------
> Sergei
> 
> 
> > martin at ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs 
> > import Distribution.Simple
> > 
> > 
> > main = defaultMain
> > 
> > 
> > martin at ubuntu:~/adga2/stdlib/agda-stdlib$ ls
> > agda-stdlib.agda-lib  GenerateEverything.hs  LICENCE
> >  README.md
> > AllNonAsciiChars.hs   GNUmakefile            notes
> >  Setup.hs
> > CHANGELOG             Header                 publish-listings.sh  src
> > doc                   index.sh               README
> > ffi                   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/4f113fa8/attachment.html