[Agda] how to run helloworld in agda

Andrea Vezzosi sanzhiyan at gmail.com
Wed Dec 9 19:17:54 CET 2015 

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

More information about the Agda mailing list