[Agda] how to run helloworld in agda

Sat Dec 19 09:40:16 CET 2015

Hi ,
how to  -i  two  difference  source directory?
time agda -c hello.agda -i. -iagda-prelude/src -iagda-stdlib/src --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs
got  error  when  run  above  command,  would like to display  some simple  result  when  using Algebra  library in stdlibrary,  
maude  have  command  to  run the function in interactive,  how  can  agda  run  command  to  test the  function  in  agda file?
agdai).    Skipping Relation.Nullary (/home/martin/hilbertreborn/agda-stdlib/src/Relation/Nullary.agdai).   Skipping Data.Product (/home/martin/hilbertreborn/agda-stdlib/src/Data/Product.agdai).   Checking Data.Sum (/home/martin/hilbertreborn/agda-stdlib/src/Data/Sum.agda).    Checking Data.Maybe.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).     Checking Data.Bool.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda)./home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5-5/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5: Parse errorCOMPILED_DATA_UHC<ERROR> Bool __BOOL__ __TRUE__ __FALS...
real	0m0.978suser	0m0.220ssys	0m0.304smartin at ubuntu:~/hilbertreborn$

Regards,
Martin 

From: tesleft at hotmail.com
To: leo at halfaya.org; ulf.norell at gmail.com
CC: sanzhiyan at gmail.com; agda at lists.chalmers.se
Subject: RE: [Agda] how to run helloworld in agda
Date: Sat, 19 Dec 2015 16:23:46 +0800

Hi  
i use FFI in  agda-stdlib , it has  error,  
1.  when  to use  Data/FFI.hs   and  when  to use  IO/FFI.hs ?
why  
time agda -c hello.agda -i. -iagda-stdlib/src/ --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
open import IOmain = putStrLn "Hello World"

martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/ --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hsChecking hello (/home/martin/hilbertreborn/hello.agda). Checking IO (/home/martin/hilbertreborn/agda-stdlib/src/IO.agda).  Checking Coinduction (/home/martin/hilbertreborn/agda-stdlib/src/Coinduction.agda).   Checking Level (/home/martin/hilbertreborn/agda-stdlib/src/Level.agda).   Finished Level.  Finished Coinduction.  Checking Data.Unit (/home/martin/hilbertreborn/agda-stdlib/src/Data/Unit.agda).   Checking Data.Sum (/home/martin/hilbertreborn/agda-stdlib/src/Data/Sum.agda).    Checking Function (/home/martin/hilbertreborn/agda-stdlib/src/Function.agda).    Finished Function.    Checking Data.Maybe.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).     Checking Data.Bool.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda)./home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5-5/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5: Parse errorCOMPILED_DATA_UHC<ERROR> Bool __BOOL__ __TRUE__ __FALS...
real	0m0.321suser	0m0.136ssys	0m0.048s

i  run  below , got  errortime agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/Data/FFI.hstime agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
open import Primitivemain = putStrLn "Hello World"
martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/Data/FFI.hsChecking hello (/home/martin/hilbertreborn/hello.agda). Checking Primitive (/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda)./home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5-5/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5: Parse errorCOMPILED_UHC<ERROR> return (\_ _ x -> UHC.Agda.Bu...
real	0m0.246suser	0m0.012ssys	0m0.020smartin at ubuntu:~/hilbertreborn$ lsagda-prelude  coq-8.4pl6         GeoCoq      MAlonzoagda-stdlib   coq-8.4pl6.tar.gz  hello.agdamartin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hsChecking hello (/home/martin/hilbertreborn/hello.agda). Checking Primitive (/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda)./home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5-5/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5: Parse errorCOMPILED_UHC<ERROR> return (\_ _ x -> UHC.Agda.Bu...
real	0m0.062suser	0m0.008ssys	0m0.016s

Regards,
Martin 

Date: Wed, 9 Dec 2015 10:36:29 -0800
Subject: Re: [Agda] how to run helloworld in agda
From: leo at halfaya.org
To: ulf.norell at gmail.com
CC: sanzhiyan at gmail.com; tesleft at hotmail.com; agda at lists.chalmers.se

Andrea:  Thanks, running cabal install as you suggest did indeed fix the ghc problem.
Ulf: Thanks as well, I didn't know about your prelude and that does indeed simplify matters considerably.  It worked beautifully for me.
Kidding aside, Agda is my favorite language and it's great to see some effort going into the practical side as well.
John
On Wed, Dec 9, 2015 at 10:23 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
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 --versionAgda version 2.4.2.4
$ git clone https://github.com/UlfNorell/agda-prelude -b compat-2.4.2Cloning into 'agda-prelude'...[...]
$ cat Hello.agdaopen import Preludemain = 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
$ ./HelloHello 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/20151219/1056a82f/attachment-0001.html