<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&#39;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&#39;s great to see some effort going into the practical side as well.</div><div><br></div><div>John</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 9, 2015 at 10:23 AM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@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"><div dir="ltr">I feel this might be a good time to plug my alternative to the standard library. Here&#39;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 &#39;agda-prelude&#39;...</div><div>[...]</div><div><br></div><div>$ cat Hello.agda</div><div>open import Prelude</div><div>main = putStrLn &quot;Hello World&quot;</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="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 9, 2015 at 7:17 PM, 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">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 &quot;cabal install&quot; from inside<br>
&quot;/Users/leo/agda/agda-stdlib-0.11/ffi&quot; ? 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 &lt;<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>&gt; wrote:<br>
&gt; I&#39;ve been following this thread and also had trouble getting hello world to<br>
&gt; work even with the advice given so far.  Here&#39;s what worked for me.<br>
&gt;<br>
&gt; My work is in /Users/leo/agda.  Here are the commands with the full paths<br>
&gt; for clarity.  First I run<br>
&gt;<br>
&gt; agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src --compile<br>
&gt; /users/leo/agda/Hello.agda<br>
&gt;<br>
&gt; This gives an error:<br>
&gt;<br>
&gt; Calling: ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda -main-is<br>
&gt; MAlonzo.Code.Hello /Users/leo/agda/MAlonzo/Code/Hello.hs --make<br>
&gt; -fwarn-incomplete-patterns -fno-warn-overlapping-patterns<br>
&gt; Compilation error:<br>
&gt;<br>
&gt; MAlonzo/Code/Foreign/Haskell.hs:4:18:<br>
&gt;     Could not find module ‘Data.FFI’<br>
&gt;     Use -v to see a list of the files searched for.<br>
&gt;<br>
&gt; MAlonzo/Code/Foreign/Haskell.hs:5:18:<br>
&gt;     Could not find module ‘IO.FFI’<br>
&gt;     Use -v to see a list of the files searched for.<br>
&gt;<br>
&gt; Trying to add FFI as follows does not pass the flag correctly to GHC:<br>
&gt;<br>
&gt; agda -i/Users/leo/agda -i/Users/leo/agda/agda-stdlib-0.11/src<br>
&gt; -i/Users/leo/agda/agda-stdlib-0.11/ffi --compile /users/leo/agda/Hello.agda<br>
&gt;<br>
&gt; So I had to add it and run ghc manually:<br>
&gt;<br>
&gt; ghc -O -o /Users/leo/agda/Hello -Werror -i/Users/leo/agda<br>
&gt; -i/Users/leo/agda/agda-stdlib-0.11/ffi  -main-is MAlonzo.Code.Hello<br>
&gt; /Users/leo/agda/MAlonzo/Code/Hello.hs --make -fwarn-incomplete-patterns<br>
&gt; -fno-warn-overlapping-patterns<br>
&gt;<br>
&gt; This finally worked!  Note that I removed the &quot;module XX where&quot; line from<br>
&gt; Hello.agda and it worked in that form.<br>
&gt;<br>
&gt; I think Agda has to win the award as the serious language which requires the<br>
&gt; most work to write hello world.<br>
&gt;<br>
&gt; John<br>
&gt;<br>
&gt;<br>
&gt; On Wed, Dec 9, 2015 at 7:02 AM, Andrea Vezzosi &lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; The agda files for the stdlib are going to be in<br>
&gt;&gt; &quot;/home/martin/adga2/agda-stadlib/src/&quot; so that&#39;s what you should use<br>
&gt;&gt; for the -i option.<br>
&gt;&gt;<br>
&gt;&gt; The haskell library in &quot;/home/martin/adga2/agda-stadlib/ffi/&quot; is<br>
&gt;&gt; needed when you compile some program using the MAlonzo haskell<br>
&gt;&gt; backend, which is the default one.<br>
&gt;&gt;<br>
&gt;&gt; If you actually want to run something like an helloworld you have to<br>
&gt;&gt; compile it first.<br>
&gt;&gt;<br>
&gt;&gt; bash$ agda -i/home/martin/adga2/agda-stadlib/ffi/ -i. --compile ag.agda<br>
&gt;&gt;<br>
&gt;&gt; If you get problems try changing &quot;module ag where&quot; to &quot;module Main where&quot;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On Wed, Dec 9, 2015 at 3:23 PM, Mandy Martino &lt;<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>&gt; wrote:<br>
&gt;&gt; &gt; after untar  <a href="https://agda.github.io/agda-stdlib" rel="noreferrer" target="_blank">https://agda.github.io/agda-stdlib</a><br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; into  directory<br>
&gt;&gt; &gt; /home/martin/adga2/agda-stadlib<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; cd  ffi<br>
&gt;&gt; &gt; cabal install Setup.hs<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; does it mean that the  extracted  file path is the library  path ?<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; /home/martin/adga2/agda-stadlib ?<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; Regards,<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" target="_blank">mechvel@botik.ru</a><br>
&gt;&gt; &gt;&gt; To: <a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a><br>
&gt;&gt; &gt;&gt; CC: <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
&gt;&gt; &gt;&gt; Date: Wed, 9 Dec 2015 15:41:17 +0400<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; On Wed, 2015-12-09 at 19:11 +0800, Mandy Martino wrote:<br>
&gt;&gt; &gt;&gt; &gt; Hi,<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; how to find the path of stdlib after it install ?<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; For example, I have installed Standard library in<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; /home/mechvel/agda/stLib/oct29-2015/src,<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; so that this directory contains Algebra.agda, and other .agda files and<br>
&gt;&gt; &gt;&gt; subdirectories.<br>
&gt;&gt; &gt;&gt; Agda is called as<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; agda -c $agdaLibOpt MyProgram.agda<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; where $agdaLibOpt is<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; -i . -i /home/mechvel/agda/stLib/oct29-2015/src -i /home/mechvel/source<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; It lists 3 paths. The last path points to where reside my .agda files<br>
&gt;&gt; &gt;&gt; which MyProgram imports.<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; &gt; martin@ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs<br>
&gt;&gt; &gt;&gt; &gt; import Distribution.Simple<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; main = defaultMain<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; martin@ubuntu:~/adga2/stdlib/agda-stdlib$ ls<br>
&gt;&gt; &gt;&gt; &gt; agda-stdlib.agda-lib GenerateEverything.hs LICENCE<br>
&gt;&gt; &gt;&gt; &gt; README.md<br>
&gt;&gt; &gt;&gt; &gt; AllNonAsciiChars.hs GNUmakefile notes<br>
&gt;&gt; &gt;&gt; &gt; Setup.hs<br>
&gt;&gt; &gt;&gt; &gt; CHANGELOG Header publish-listings.sh src<br>
&gt;&gt; &gt;&gt; &gt; doc index.sh README<br>
&gt;&gt; &gt;&gt; &gt; ffi lib.cabal README.agda<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; Regards,<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; Martin<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; Subject: Re: [Agda] how to run helloworld in agda<br>
&gt;&gt; &gt;&gt; &gt; &gt; From: <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a><br>
&gt;&gt; &gt;&gt; &gt; &gt; To: <a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a><br>
&gt;&gt; &gt;&gt; &gt; &gt; CC: <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
&gt;&gt; &gt;&gt; &gt; &gt; Date: Tue, 8 Dec 2015 21:06:16 +0400<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; The interactive mode is no longer supported. Don&#39;t complain if it<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; doesn&#39;t work.<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; Main&gt; :l ag.agda<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; Checking ag (/home/martin/adga2/ag.agda).<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; /home/martin/adga2/ag.agda:3,13-25<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; Failed to find source of module IO.Primitive in any of the<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; following locations:<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; /home/martin/adga2/IO/Primitive.agda<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; /home/martin/adga2/IO/Primitive.lagda<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &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; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &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; &gt; &gt; when scope checking the declaration<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; Failed.<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; Main&gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; module ag where<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; open import Data.String using (toCostring; String)<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; open import Foreign.Haskell using (Unit)<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; main : IO Unit<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; main = putStrLn (toCostring &quot;Hello, Agda!&quot;)<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; I remove &quot;module ag where&quot; (because this module has `main&#39; in it),<br>
&gt;&gt; &gt;&gt; &gt; &gt; and apply<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; agda -c $agdaLibOpt Hello.agda<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; where $agdaLibOpt contains the path to the /src directory of<br>
&gt;&gt; &gt;&gt; &gt; &gt; Standard library.<br>
&gt;&gt; &gt;&gt; &gt; &gt; This makes the executable file Hello.<br>
&gt;&gt; &gt;&gt; &gt; &gt; Then, the command<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; ./Hello<br>
&gt;&gt; &gt;&gt; &gt; &gt; prints<br>
&gt;&gt; &gt;&gt; &gt; &gt; &quot;Hello, Agda!&quot;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; why use open import, but not import<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; After &quot;import Foo&quot;,<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; one can write Foo.foo, if foo is defined in Foo module.<br>
&gt;&gt; &gt;&gt; &gt; &gt; After<br>
&gt;&gt; &gt;&gt; &gt; &gt; import Foo<br>
&gt;&gt; &gt;&gt; &gt; &gt; open Foo using (foo)<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; one can write `foo&#39; in the scope.<br>
&gt;&gt; &gt;&gt; &gt; &gt; And the line<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; open import Foo using (foo)<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; combines the above lines of `import&#39; and `open&#39;.<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; Regards,<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; ------<br>
&gt;&gt; &gt;&gt; &gt; &gt; Sergei<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; _______________________________________________<br>
&gt;&gt; &gt; Agda mailing list<br>
&gt;&gt; &gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt;&gt; &gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt; &gt;<br>
&gt;&gt; _______________________________________________<br>
&gt;&gt; Agda mailing list<br>
&gt;&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt;&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>
&gt;<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>