<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:·s²Ó©úÅé
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi </font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><span style="font-size: 12pt;">i use FFI in agda-stdlib , it has error, </span></div><div><br></div><div>1. when to use Data/FFI.hs and when to use IO/FFI.hs ?</div><div><span style="font-size: 12pt;"><br></span></div><div>why </div><div><font color="#000000"><div><br></div><div><div><span style="font-size: 12pt;">time agda -c hello.agda -i. -iagda-stdlib/src/ --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs</span></div></div><div><br></div><div><div>open import IO</div><div>main = putStrLn "Hello World"</div></div><div><br></div><div><br></div><div><div>martin@ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/ --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs</div><div>Checking hello (/home/martin/hilbertreborn/hello.agda).</div><div> Checking IO (/home/martin/hilbertreborn/agda-stdlib/src/IO.agda).</div><div> Checking Coinduction (/home/martin/hilbertreborn/agda-stdlib/src/Coinduction.agda).</div><div> Checking Level (/home/martin/hilbertreborn/agda-stdlib/src/Level.agda).</div><div> Finished Level.</div><div> Finished Coinduction.</div><div> Checking Data.Unit (/home/martin/hilbertreborn/agda-stdlib/src/Data/Unit.agda).</div><div> Checking Data.Sum (/home/martin/hilbertreborn/agda-stdlib/src/Data/Sum.agda).</div><div> Checking Function (/home/martin/hilbertreborn/agda-stdlib/src/Function.agda).</div><div> Finished Function.</div><div> Checking Data.Maybe.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).</div><div> Checking Data.Bool.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda).</div><div>/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5-5</div><div>/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5: Parse error</div><div>COMPILED_DATA_UHC<ERROR></div><div> Bool __BOOL__ __TRUE__ __FALS...</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.321s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.136s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.048s</div></div><div><br></div><div><br></div><div><br></div><div>i run below , got error</div></font></div><div><font color="#000000"><div>time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/Data/FFI.hs</div><div>time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs</div><div style="font-size: 12pt;"><br></div><div style="font-size: 12pt;"><div style="font-size: 12pt;">open import Primitive</div><div style="font-size: 12pt;">main = putStrLn "Hello World"</div></div><div style="font-size: 12pt;"><br></div><div><div><div>martin@ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/Data/FFI.hs</div><div>Checking hello (/home/martin/hilbertreborn/hello.agda).</div><div> Checking Primitive (/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda).</div><div>/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5-5</div><div>/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5: Parse error</div><div>COMPILED_UHC<ERROR></div><div> return (\_ _ x -> UHC.Agda.Bu...</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.246s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.012s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.020s</div><div>martin@ubuntu:~/hilbertreborn$ ls</div><div>agda-prelude coq-8.4pl6 GeoCoq MAlonzo</div><div>agda-stdlib coq-8.4pl6.tar.gz hello.agda</div><div>martin@ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib/src/IO --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs</div><div>Checking hello (/home/martin/hilbertreborn/hello.agda).</div><div> Checking Primitive (/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda).</div><div>/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5-5</div><div>/home/martin/hilbertreborn/agda-stdlib/src/IO/Primitive.agda:31,5: Parse error</div><div>COMPILED_UHC<ERROR></div><div> return (\_ _ x -> UHC.Agda.Bu...</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.062s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.008s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m0.016s</div></div><div><br></div><div style="font-size: 12pt;"><br></div></div></font><div>Regards,</div><div><br></div><div>Martin </div><br><br><div><hr id="stopSpelling">Date: Wed, 9 Dec 2015 10:36:29 -0800<br>Subject: Re: [Agda] how to run helloworld in agda<br>From: leo@halfaya.org<br>To: ulf.norell@gmail.com<br>CC: sanzhiyan@gmail.com; tesleft@hotmail.com; agda@lists.chalmers.se<br><br><div dir="ltr">Andrea: Thanks, running cabal install as you suggest did indeed fix the ghc problem.<div><br></div><div>Ulf: Thanks as well, I didn't know about your prelude and that does indeed simplify matters considerably. It worked beautifully for me.</div><div><br></div><div>Kidding aside, Agda is my favorite language and it's great to see some effort going into the practical side as well.</div><div><br></div><div>John</div></div><div class="ecxgmail_extra"><br><div class="ecxgmail_quote">On Wed, Dec 9, 2015 at 10:23 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="ecxgmail_quote" style="border-left:1px #ccc solid;padding-left:1ex;"><div dir="ltr">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 (<a href="https://github.com/UlfNorell/agda-prelude" target="_blank">https://github.com/UlfNorell/agda-prelude</a>):<div><br></div><div><div>$ agda --version</div><div>Agda version 2.4.2.4</div><div><br></div><div>$ git clone <a href="https://github.com/UlfNorell/agda-prelude" target="_blank">https://github.com/UlfNorell/agda-prelude</a> -b compat-2.4.2</div><div>Cloning into 'agda-prelude'...</div><div>[...]</div><div><br></div><div>$ cat Hello.agda</div><div>open import Prelude</div><div>main = putStrLn "Hello World"</div><div><br></div><div>$ time agda -c Hello.agda -i. -iagda-prelude/src --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs</div><div>[...]</div><div>Linking /Users/ulfn/research/scratch/tmp/Hello ...</div><div>user<span style="white-space:pre-wrap;"> </span>0m7.155s</div><div><br></div><div>$ ./Hello</div><div>Hello World</div><div><br></div><div>$ ll Hello</div><div>-rwxr-xr-x 1 ulfn staff 1981612 Dec 9 19:18 Hello</div></div><span class="ecxHOEnZb"><font color="#888888"><div><br></div><div>/ Ulf</div></font></span></div><div class="ecxHOEnZb"><div class="h5"><div class="ecxgmail_extra"><br><div class="ecxgmail_quote">On Wed, Dec 9, 2015 at 7:17 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="ecxgmail_quote" style="border-left:1px #ccc solid;padding-left:1ex;">I guess my instructions were assuming a few things, and the whole<br>
process is surely more complicated than it could be.<br>
<br>
However, have you run "cabal install" from inside<br>
"/Users/leo/agda/agda-stdlib-0.11/ffi" ? That should make the Data.FFI<br>
module available without specifying include paths to ghc directly.<br>
<div><div><br>
On Wed, Dec 9, 2015 at 6:05 PM, John Leo <<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>> wrote:<br>
> I've been following this thread and also had trouble getting hello world to<br>
> work even with the advice given so far. Here's what worked for me.<br>
><br>
> My work is in /Users/leo/agda. Here are the commands with the full paths<br>
> for clarity. First I run<br>
><br>
> agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src --compile<br>
> /users/leo/agda/Hello.agda<br>
><br>
> This gives an error:<br>
><br>
> Calling: ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda -main-is<br>
> MAlonzo.Code.Hello /Users/leo/agda/MAlonzo/Code/Hello.hs --make<br>
> -fwarn-incomplete-patterns -fno-warn-overlapping-patterns<br>
> Compilation error:<br>
><br>
> MAlonzo/Code/Foreign/Haskell.hs:4:18:<br>
> Could not find module ¡¥Data.FFI¡¦<br>
> Use -v to see a list of the files searched for.<br>
><br>
> MAlonzo/Code/Foreign/Haskell.hs:5:18:<br>
> Could not find module ¡¥IO.FFI¡¦<br>
> Use -v to see a list of the files searched for.<br>
><br>
> Trying to add FFI as follows does not pass the flag correctly to GHC:<br>
><br>
> agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src<br>
> -i/Users/leo/agda/agda-stdlib-0.11/ffi --compile /users/leo/agda/Hello.agda<br>
><br>
> So I had to add it and run ghc manually:<br>
><br>
> ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda<br>
> -i/Users/leo/agda/agda-stdlib-0.11/ffi -main-is MAlonzo.Code.Hello<br>
> /Users/leo/agda/MAlonzo/Code/Hello.hs --make -fwarn-incomplete-patterns<br>
> -fno-warn-overlapping-patterns<br>
><br>
> This finally worked! Note that I removed the "module XX where" line from<br>
> Hello.agda and it worked in that form.<br>
><br>
> I think Agda has to win the award as the serious language which requires the<br>
> most work to write hello world.<br>
><br>
> John<br>
><br>
><br>
> On Wed, Dec 9, 2015 at 7:02 AM, Andrea Vezzosi <<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>> wrote:<br>
>><br>
>> The agda files for the stdlib are going to be in<br>
>> "/home/martin/adga2/agda-stadlib/src/" so that's what you should use<br>
>> for the -i option.<br>
>><br>
>> The haskell library in "/home/martin/adga2/agda-stadlib/ffi/" is<br>
>> needed when you compile some program using the MAlonzo haskell<br>
>> backend, which is the default one.<br>
>><br>
>> If you actually want to run something like an helloworld you have to<br>
>> compile it first.<br>
>><br>
>> bash$ agda -i/home/martin/adga2/agda-stadlib/ffi/ -i. --compile ag.agda<br>
>><br>
>> If you get problems try changing "module ag where" to "module Main where"<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>> On Wed, Dec 9, 2015 at 3:23 PM, Mandy Martino <<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>> wrote:<br>
>> > after untar <a href="https://agda.github.io/agda-stdlib" rel="noreferrer" target="_blank">https://agda.github.io/agda-stdlib</a><br>
>> ><br>
>> > into directory<br>
>> > /home/martin/adga2/agda-stadlib<br>
>> ><br>
>> > cd ffi<br>
>> > cabal install Setup.hs<br>
>> ><br>
>> > does it mean that the extracted file path is the library path ?<br>
>> ><br>
>> > /home/martin/adga2/agda-stadlib ?<br>
>> ><br>
>> > Regards,<br>
>> ><br>
>> > Martin<br>
>> ><br>
>> ><br>
>> >> Subject: RE: [Agda] how to run helloworld in agda<br>
>> >> From: <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a><br>
>> >> To: <a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a><br>
>> >> CC: <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
>> >> Date: Wed, 9 Dec 2015 15:41:17 +0400<br>
>> >><br>
>> >> On Wed, 2015-12-09 at 19:11 +0800, Mandy Martino wrote:<br>
>> >> > Hi,<br>
>> >> ><br>
>> >> ><br>
>> >> > how to find the path of stdlib after it install ?<br>
>> >> ><br>
>> >><br>
>> >> For example, I have installed Standard library in<br>
>> >><br>
>> >> /home/mechvel/agda/stLib/oct29-2015/src,<br>
>> >><br>
>> >> so that this directory contains Algebra.agda, and other .agda files and<br>
>> >> subdirectories.<br>
>> >> Agda is called as<br>
>> >><br>
>> >> agda -c $agdaLibOpt MyProgram.agda<br>
>> >><br>
>> >> where $agdaLibOpt is<br>
>> >><br>
>> >> -i . -i /home/mechvel/agda/stLib/oct29-2015/src -i /home/mechvel/source<br>
>> >><br>
>> >> It lists 3 paths. The last path points to where reside my .agda files<br>
>> >> which MyProgram imports.<br>
>> >><br>
>> >> ------<br>
>> >> Sergei<br>
>> >><br>
>> >><br>
>> >> > martin@ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs<br>
>> >> > import Distribution.Simple<br>
>> >> ><br>
>> >> ><br>
>> >> > main = defaultMain<br>
>> >> ><br>
>> >> ><br>
>> >> > martin@ubuntu:~/adga2/stdlib/agda-stdlib$ ls<br>
>> >> > agda-stdlib.agda-lib GenerateEverything.hs LICENCE<br>
>> >> > README.md<br>
>> >> > AllNonAsciiChars.hs GNUmakefile notes<br>
>> >> > Setup.hs<br>
>> >> > CHANGELOG Header publish-listings.sh src<br>
>> >> > doc index.sh README<br>
>> >> > ffi lib.cabal README.agda<br>
>> >> ><br>
>> >> ><br>
>> >> ><br>
>> >> > Regards,<br>
>> >> ><br>
>> >> ><br>
>> >> > Martin<br>
>> >> ><br>
>> >> ><br>
>> >> > > Subject: Re: [Agda] how to run helloworld in agda<br>
>> >> > > From: <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a><br>
>> >> > > To: <a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a><br>
>> >> > > CC: <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
>> >> > > Date: Tue, 8 Dec 2015 21:06:16 +0400<br>
>> >> > ><br>
>> >> > > On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:<br>
>> >> > > > The interactive mode is no longer supported. Don't complain if it<br>
>> >> > > > doesn't work.<br>
>> >> > > > Main> :l ag.agda<br>
>> >> > > > Checking ag (/home/martin/adga2/ag.agda).<br>
>> >> > > > /home/martin/adga2/ag.agda:3,13-25<br>
>> >> > > > Failed to find source of module IO.Primitive in any of the<br>
>> >> > > > following locations:<br>
>> >> > > > /home/martin/adga2/IO/Primitive.agda<br>
>> >> > > > /home/martin/adga2/IO/Primitive.lagda<br>
>> >> > ><br>
>> >> > ><br>
>> >> > ><br>
>> >> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br>
>> >> > ><br>
>> >> > ><br>
>> >> > ><br>
>> >> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda<br>
>> >> > > > when scope checking the declaration<br>
>> >> > > > open import IO.Primitive using (IO; putStrLn)<br>
>> >> > > > Failed.<br>
>> >> > > > Main><br>
>> >> > > ><br>
>> >> > > > module ag where<br>
>> >> > > ><br>
>> >> > > > open import IO.Primitive using (IO; putStrLn)<br>
>> >> > > > open import Data.String using (toCostring; String)<br>
>> >> > > > open import Foreign.Haskell using (Unit)<br>
>> >> > > ><br>
>> >> > > > main : IO Unit<br>
>> >> > > > main = putStrLn (toCostring "Hello, Agda!")<br>
>> >> > > ><br>
>> >> > ><br>
>> >> > > I remove "module ag where" (because this module has `main' in it),<br>
>> >> > > and apply<br>
>> >> > ><br>
>> >> > > agda -c $agdaLibOpt Hello.agda<br>
>> >> > ><br>
>> >> > > where $agdaLibOpt contains the path to the /src directory of<br>
>> >> > > Standard library.<br>
>> >> > > This makes the executable file Hello.<br>
>> >> > > Then, the command<br>
>> >> > ><br>
>> >> > > ./Hello<br>
>> >> > > prints<br>
>> >> > > "Hello, Agda!"<br>
>> >> > ><br>
>> >> > ><br>
>> >> > > > why use open import, but not import<br>
>> >> > ><br>
>> >> > > After "import Foo",<br>
>> >> > ><br>
>> >> > > one can write Foo.foo, if foo is defined in Foo module.<br>
>> >> > > After<br>
>> >> > > import Foo<br>
>> >> > > open Foo using (foo)<br>
>> >> > ><br>
>> >> > > one can write `foo' in the scope.<br>
>> >> > > And the line<br>
>> >> > ><br>
>> >> > > open import Foo using (foo)<br>
>> >> > ><br>
>> >> > > combines the above lines of `import' and `open'.<br>
>> >> > ><br>
>> >> > > Regards,<br>
>> >> > ><br>
>> >> > > ------<br>
>> >> > > Sergei<br>
>> >> > ><br>
>> >> > ><br>
>> >> > ><br>
>> >> ><br>
>> >><br>
>> >><br>
>> ><br>
>> > _______________________________________________<br>
>> > Agda mailing list<br>
>> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> ><br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div></div></div> </div></body>
</html>