[Agda] how to run helloworld in agda

Ulf Norell ulf.norell at gmail.com
Wed Dec 9 19:23:05 CET 2015 

I feel this might be a good time to plug my alternative to the standard
library. Here's the steps to get hello world running with agda-prelude (
https://github.com/UlfNorell/agda-prelude):

$ agda --version
Agda version 2.4.2.4

$ git clone https://github.com/UlfNorell/agda-prelude -b compat-2.4.2
Cloning into 'agda-prelude'...
[...]

$ cat Hello.agda
open import Prelude
main = putStrLn "Hello World"

$ time agda -c Hello.agda -i. -iagda-prelude/src
--ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs
[...]
Linking /Users/ulfn/research/scratch/tmp/Hello ...
user 0m7.155s

$ ./Hello
Hello World

$ ll Hello
-rwxr-xr-x  1 ulfn  staff  1981612 Dec  9 19:18 Hello

/ Ulf

On Wed, Dec 9, 2015 at 7:17 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> I guess my instructions were assuming a few things, and the whole
> process is surely more complicated than it could be.
>
> However, have you run "cabal install" from inside
> "/Users/leo/agda/agda-stdlib-0.11/ffi" ? That should make the Data.FFI
> module available without specifying include paths to ghc directly.
>
> On Wed, Dec 9, 2015 at 6:05 PM, John Leo <leo at halfaya.org> wrote:
> > 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
> >
> >
> _______________________________________________
> 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/71cd2d24/attachment-0001.html

More information about the Agda mailing list