<div dir="ltr">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.<div><br></div><div>My work is in /Users/leo/agda. Here are the commands with the full paths for clarity. First I run</div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src --compile /users/leo/agda/Hello.agda</font><br></div></div><div><br></div><div>This gives an error:</div><div><br></div><div><div><font face="monospace, monospace">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</font></div><div><font face="monospace, monospace">Compilation error:</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">MAlonzo/Code/Foreign/Haskell.hs:4:18:</font></div><div><font face="monospace, monospace"> Could not find module ‘Data.FFI’</font></div><div><font face="monospace, monospace"> Use -v to see a list of the files searched for.</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">MAlonzo/Code/Foreign/Haskell.hs:5:18:</font></div><div><font face="monospace, monospace"> Could not find module ‘IO.FFI’</font></div><div><font face="monospace, monospace"> Use -v to see a list of the files searched for.</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">Trying to add FFI as follows does not pass the flag correctly to GHC:</font></div><div><br></div><div><font face="monospace, monospace">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</font><br></div><div><br></div><div>So I had to add it and run ghc manually:</div><div><br></div><div><font face="monospace, monospace">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</font><br></div><div><br></div><div>This finally worked! Note that I removed the "module XX where" line from Hello.agda and it worked in that form.</div><div><br></div><div>I think Agda has to win the award as the serious language which requires the most work to write hello world.</div><div><br></div><div>John</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 9, 2015 at 7:02 AM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
<br>
On Wed, Dec 9, 2015 at 3:23 PM, Mandy Martino <<a href="mailto:tesleft@hotmail.com">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">mechvel@botik.ru</a><br>
>> To: <a href="mailto:tesleft@hotmail.com">tesleft@hotmail.com</a><br>
>> CC: <a href="mailto:agda@lists.chalmers.se">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">mechvel@botik.ru</a><br>
>> > > To: <a href="mailto:tesleft@hotmail.com">tesleft@hotmail.com</a><br>
>> > > CC: <a href="mailto:agda@lists.chalmers.se">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>
>> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<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>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">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">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>