[Agda] how to run helloworld in agda
John Leo
leo at halfaya.org
Wed Dec 9 18:05:06 CET 2015
I've been following this thread and also had trouble getting hello world to
work even with the advice given so far. Here's what worked for me.
My work is in /Users/leo/agda. Here are the commands with the full paths
for clarity. First I run
agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src --compile
/users/leo/agda/Hello.agda
This gives an error:
Calling: ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda -main-is
MAlonzo.Code.Hello /Users/leo/agda/MAlonzo/Code/Hello.hs --make
-fwarn-incomplete-patterns -fno-warn-overlapping-patterns
Compilation error:
MAlonzo/Code/Foreign/Haskell.hs:4:18:
Could not find module ‘Data.FFI’
Use -v to see a list of the files searched for.
MAlonzo/Code/Foreign/Haskell.hs:5:18:
Could not find module ‘IO.FFI’
Use -v to see a list of the files searched for.
Trying to add FFI as follows does not pass the flag correctly to GHC:
agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src
-i/Users/leo/agda/agda-stdlib-0.11/ffi --compile /users/leo/agda/Hello.agda
So I had to add it and run ghc manually:
ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda
-i/Users/leo/agda/agda-stdlib-0.11/ffi -main-is MAlonzo.Code.Hello
/Users/leo/agda/MAlonzo/Code/Hello.hs --make -fwarn-incomplete-patterns
-fno-warn-overlapping-patterns
This finally worked! Note that I removed the "module XX where" line from
Hello.agda and it worked in that form.
I think Agda has to win the award as the serious language which requires
the most work to write hello world.
John
On Wed, Dec 9, 2015 at 7:02 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> The agda files for the stdlib are going to be in
> "/home/martin/adga2/agda-stadlib/src/" so that's what you should use
> for the -i option.
>
> The haskell library in "/home/martin/adga2/agda-stadlib/ffi/" is
> needed when you compile some program using the MAlonzo haskell
> backend, which is the default one.
>
> If you actually want to run something like an helloworld you have to
> compile it first.
>
> bash$ agda -i/home/martin/adga2/agda-stadlib/ffi/ -i. --compile ag.agda
>
> If you get problems try changing "module ag where" to "module Main where"
>
>
>
>
>
> On Wed, Dec 9, 2015 at 3:23 PM, Mandy Martino <tesleft at hotmail.com> wrote:
> > after untar https://agda.github.io/agda-stdlib
> >
> > into directory
> > /home/martin/adga2/agda-stadlib
> >
> > cd ffi
> > cabal 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
> >> > >
> >> > >
> >> > >
> >> >
> >>
> >>
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151209/9f71db73/attachment.html
More information about the Agda
mailing list