[Agda] how to run helloworld in agda

[Sergei Meshveliani]

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
> > 
> > 
> > 
>