[Agda] how to run helloworld in agda
Mandy Martino
tesleft at hotmail.com
Wed Dec 9 15:19:39 CET 2015
i still not understand this,
after untar the tar.gz file to /home/martin/adga2/agda-stdlib,
i use
cd fficabal install Setup.hs
does it mean that the library path is in /home/martin/adga2/agda-stdlib ?
https://github.com/agda/agda-stdlib
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/7d1b8402/attachment-0001.html
More information about the Agda
mailing list