<div dir="ltr">I&#39;ve been following this thread and also had trouble getting hello world to work even with the advice given so far.  Here&#39;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 &quot;module XX where&quot; 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">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</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>
&quot;/home/martin/adga2/agda-stadlib/src/&quot; so that&#39;s what you should use<br>
for the -i option.<br>
<br>
The haskell library in &quot;/home/martin/adga2/agda-stadlib/ffi/&quot; 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 &quot;module ag where&quot; to &quot;module Main where&quot;<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
<br>
On Wed, Dec 9, 2015 at 3:23 PM, Mandy Martino &lt;<a href="mailto:tesleft@hotmail.com">tesleft@hotmail.com</a>&gt; wrote:<br>
&gt; after untar  <a href="https://agda.github.io/agda-stdlib" rel="noreferrer" target="_blank">https://agda.github.io/agda-stdlib</a><br>
&gt;<br>
&gt; into  directory<br>
&gt; /home/martin/adga2/agda-stadlib<br>
&gt;<br>
&gt; cd  ffi<br>
&gt; cabal install Setup.hs<br>
&gt;<br>
&gt; does it mean that the  extracted  file path is the library  path ?<br>
&gt;<br>
&gt; /home/martin/adga2/agda-stadlib ?<br>
&gt;<br>
&gt; Regards,<br>
&gt;<br>
&gt; Martin<br>
&gt;<br>
&gt;<br>
&gt;&gt; Subject: RE: [Agda] how to run helloworld in agda<br>
&gt;&gt; From: <a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a><br>
&gt;&gt; To: <a href="mailto:tesleft@hotmail.com">tesleft@hotmail.com</a><br>
&gt;&gt; CC: <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
&gt;&gt; Date: Wed, 9 Dec 2015 15:41:17 +0400<br>
&gt;&gt;<br>
&gt;&gt; On Wed, 2015-12-09 at 19:11 +0800, Mandy Martino wrote:<br>
&gt;&gt; &gt; Hi,<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; how to find the path of stdlib after it install ?<br>
&gt;&gt; &gt;<br>
&gt;&gt;<br>
&gt;&gt; For example, I have installed Standard library in<br>
&gt;&gt;<br>
&gt;&gt; /home/mechvel/agda/stLib/oct29-2015/src,<br>
&gt;&gt;<br>
&gt;&gt; so that this directory contains Algebra.agda, and other .agda files and<br>
&gt;&gt; subdirectories.<br>
&gt;&gt; Agda is called as<br>
&gt;&gt;<br>
&gt;&gt; agda -c $agdaLibOpt MyProgram.agda<br>
&gt;&gt;<br>
&gt;&gt; where $agdaLibOpt is<br>
&gt;&gt;<br>
&gt;&gt; -i . -i /home/mechvel/agda/stLib/oct29-2015/src -i /home/mechvel/source<br>
&gt;&gt;<br>
&gt;&gt; It lists 3 paths. The last path points to where reside my .agda files<br>
&gt;&gt; which MyProgram imports.<br>
&gt;&gt;<br>
&gt;&gt; ------<br>
&gt;&gt; Sergei<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; &gt; martin@ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs<br>
&gt;&gt; &gt; import Distribution.Simple<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; main = defaultMain<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; martin@ubuntu:~/adga2/stdlib/agda-stdlib$ ls<br>
&gt;&gt; &gt; agda-stdlib.agda-lib GenerateEverything.hs LICENCE<br>
&gt;&gt; &gt; README.md<br>
&gt;&gt; &gt; AllNonAsciiChars.hs GNUmakefile notes<br>
&gt;&gt; &gt; Setup.hs<br>
&gt;&gt; &gt; CHANGELOG Header publish-listings.sh src<br>
&gt;&gt; &gt; doc index.sh README<br>
&gt;&gt; &gt; ffi lib.cabal README.agda<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; Regards,<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; Martin<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; &gt; Subject: Re: [Agda] how to run helloworld in agda<br>
&gt;&gt; &gt; &gt; From: <a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a><br>
&gt;&gt; &gt; &gt; To: <a href="mailto:tesleft@hotmail.com">tesleft@hotmail.com</a><br>
&gt;&gt; &gt; &gt; CC: <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
&gt;&gt; &gt; &gt; Date: Tue, 8 Dec 2015 21:06:16 +0400<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:<br>
&gt;&gt; &gt; &gt; &gt; The interactive mode is no longer supported. Don&#39;t complain if it<br>
&gt;&gt; &gt; &gt; &gt; doesn&#39;t work.<br>
&gt;&gt; &gt; &gt; &gt; Main&gt; :l ag.agda<br>
&gt;&gt; &gt; &gt; &gt; Checking ag (/home/martin/adga2/ag.agda).<br>
&gt;&gt; &gt; &gt; &gt; /home/martin/adga2/ag.agda:3,13-25<br>
&gt;&gt; &gt; &gt; &gt; Failed to find source of module IO.Primitive in any of the<br>
&gt;&gt; &gt; &gt; &gt; following locations:<br>
&gt;&gt; &gt; &gt; &gt; /home/martin/adga2/IO/Primitive.agda<br>
&gt;&gt; &gt; &gt; &gt; /home/martin/adga2/IO/Primitive.lagda<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda<br>
&gt;&gt; &gt; &gt; &gt; when scope checking the declaration<br>
&gt;&gt; &gt; &gt; &gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt;&gt; &gt; &gt; &gt; Failed.<br>
&gt;&gt; &gt; &gt; &gt; Main&gt;<br>
&gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; &gt; module ag where<br>
&gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; &gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt;&gt; &gt; &gt; &gt; open import Data.String using (toCostring; String)<br>
&gt;&gt; &gt; &gt; &gt; open import Foreign.Haskell using (Unit)<br>
&gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; &gt; main : IO Unit<br>
&gt;&gt; &gt; &gt; &gt; main = putStrLn (toCostring &quot;Hello, Agda!&quot;)<br>
&gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; I remove &quot;module ag where&quot; (because this module has `main&#39; in it),<br>
&gt;&gt; &gt; &gt; and apply<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; agda -c $agdaLibOpt Hello.agda<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; where $agdaLibOpt contains the path to the /src directory of<br>
&gt;&gt; &gt; &gt; Standard library.<br>
&gt;&gt; &gt; &gt; This makes the executable file Hello.<br>
&gt;&gt; &gt; &gt; Then, the command<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; ./Hello<br>
&gt;&gt; &gt; &gt; prints<br>
&gt;&gt; &gt; &gt; &quot;Hello, Agda!&quot;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; &gt; why use open import, but not import<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; After &quot;import Foo&quot;,<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; one can write Foo.foo, if foo is defined in Foo module.<br>
&gt;&gt; &gt; &gt; After<br>
&gt;&gt; &gt; &gt; import Foo<br>
&gt;&gt; &gt; &gt; open Foo using (foo)<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; one can write `foo&#39; in the scope.<br>
&gt;&gt; &gt; &gt; And the line<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; open import Foo using (foo)<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; combines the above lines of `import&#39; and `open&#39;.<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; Regards,<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt; ------<br>
&gt;&gt; &gt; &gt; Sergei<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
</div></div><div class="HOEnZb"><div class="h5">&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<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>