<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></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><font size="3" style="font-size:12pt;" color="#000000">how to &nbsp;-i &nbsp;two &nbsp;difference &nbsp;source directory?</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000">time agda -c hello.agda -i. -iagda-prelude/src -iagda-stdlib/src --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs</font></div><div><font color="#000000"><br></font></div><div>got &nbsp;error &nbsp;when &nbsp;run &nbsp;above &nbsp;command, &nbsp;would like to display &nbsp;some simple &nbsp;result &nbsp;when &nbsp;using Algebra &nbsp;library in stdlibrary, &nbsp;</div><div><br></div><div>maude &nbsp;have &nbsp;command &nbsp;to &nbsp;run the function in interactive, &nbsp;how &nbsp;can &nbsp;agda &nbsp;run &nbsp;command &nbsp;to &nbsp;test the &nbsp;function &nbsp;in &nbsp;agda file?</div><div><br></div><div><div>agdai).</div><div>&nbsp; &nbsp; Skipping Relation.Nullary (/home/martin/hilbertreborn/agda-stdlib/src/Relation/Nullary.agdai).</div><div>&nbsp; &nbsp;Skipping Data.Product (/home/martin/hilbertreborn/agda-stdlib/src/Data/Product.agdai).</div><div>&nbsp; &nbsp;Checking Data.Sum (/home/martin/hilbertreborn/agda-stdlib/src/Data/Sum.agda).</div><div>&nbsp; &nbsp; Checking Data.Maybe.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).</div><div>&nbsp; &nbsp; &nbsp;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&lt;ERROR&gt;</div><div>&nbsp;Bool __BOOL__ __TRUE__ __FALS...</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre">        </span>0m0.978s</div><div>user<span class="Apple-tab-span" style="white-space:pre">        </span>0m0.220s</div><div>sys<span class="Apple-tab-span" style="white-space:pre">        </span>0m0.304s</div><div>martin@ubuntu:~/hilbertreborn$</div></div><div><br><br><div>Regards,</div><div><br></div><div>Martin&nbsp;</div><br><br><div><hr id="stopSpelling">From: tesleft@hotmail.com<br>To: leo@halfaya.org; ulf.norell@gmail.com<br>CC: sanzhiyan@gmail.com; agda@lists.chalmers.se<br>Subject: RE: [Agda] how to run helloworld in agda<br>Date: Sat, 19 Dec 2015 16:23:46 +0800<br><br>

<style><!--
.ExternalClass .ecxhmmessage P {
padding:0px;
}

.ExternalClass body.ecxhmmessage {
font-size:12pt;
font-family:新細明體;
}

--></style>
<div dir="ltr"><font size="3" style="font-size:12pt;" color="#000000">Hi &nbsp;</font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><span style="font-size:12pt;">i use FFI in &nbsp;agda-stdlib , it has &nbsp;error, &nbsp;</span></div><div><br></div><div>1. &nbsp;when &nbsp;to use &nbsp;Data/FFI.hs &nbsp; and &nbsp;when &nbsp;to use &nbsp;IO/FFI.hs ?</div><div><span style="font-size:12pt;"><br></span></div><div>why &nbsp;</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>&nbsp;Checking IO (/home/martin/hilbertreborn/agda-stdlib/src/IO.agda).</div><div>&nbsp; Checking Coinduction (/home/martin/hilbertreborn/agda-stdlib/src/Coinduction.agda).</div><div>&nbsp; &nbsp;Checking Level (/home/martin/hilbertreborn/agda-stdlib/src/Level.agda).</div><div>&nbsp; &nbsp;Finished Level.</div><div>&nbsp; Finished Coinduction.</div><div>&nbsp; Checking Data.Unit (/home/martin/hilbertreborn/agda-stdlib/src/Data/Unit.agda).</div><div>&nbsp; &nbsp;Checking Data.Sum (/home/martin/hilbertreborn/agda-stdlib/src/Data/Sum.agda).</div><div>&nbsp; &nbsp; Checking Function (/home/martin/hilbertreborn/agda-stdlib/src/Function.agda).</div><div>&nbsp; &nbsp; Finished Function.</div><div>&nbsp; &nbsp; Checking Data.Maybe.Base (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).</div><div>&nbsp; &nbsp; &nbsp;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&lt;ERROR&gt;</div><div>&nbsp;Bool __BOOL__ __TRUE__ __FALS...</div><div><br></div><div>real<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.321s</div><div>user<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.136s</div><div>sys<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.048s</div></div><div><br></div><div><br></div><div><br></div><div>i &nbsp;run &nbsp;below , got &nbsp;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>&nbsp;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&lt;ERROR&gt;</div><div>&nbsp;return (\_ _ x -&gt; UHC.Agda.Bu...</div><div><br></div><div>real<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.246s</div><div>user<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.012s</div><div>sys<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.020s</div><div>martin@ubuntu:~/hilbertreborn$ ls</div><div>agda-prelude &nbsp;coq-8.4pl6 &nbsp; &nbsp; &nbsp; &nbsp; GeoCoq &nbsp; &nbsp; &nbsp;MAlonzo</div><div>agda-stdlib &nbsp; coq-8.4pl6.tar.gz &nbsp;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>&nbsp;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&lt;ERROR&gt;</div><div>&nbsp;return (\_ _ x -&gt; UHC.Agda.Bu...</div><div><br></div><div>real<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.062s</div><div>user<span class="ecxApple-tab-span" style="white-space:pre;">        </span>0m0.008s</div><div>sys<span class="ecxApple-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&nbsp;</div><br><br><div><hr id="ecxstopSpelling">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: &nbsp;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.&nbsp; 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">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</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 &nbsp;1 ulfn &nbsp;staff &nbsp;1981612 Dec &nbsp;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">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</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 &lt;<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>&gt; wrote:<br>
&gt; I've been following this thread and also had trouble getting hello world to<br>
&gt; work even with the advice given so far.&nbsp; Here's what worked for me.<br>
&gt;<br>
&gt; My work is in /Users/leo/agda.&nbsp; Here are the commands with the full paths<br>
&gt; for clarity.&nbsp; 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;&nbsp; &nbsp; &nbsp;Could not find module ‘Data.FFI’<br>
&gt;&nbsp; &nbsp; &nbsp;Use -v to see a list of the files searched for.<br>
&gt;<br>
&gt; MAlonzo/Code/Foreign/Haskell.hs:5:18:<br>
&gt;&nbsp; &nbsp; &nbsp;Could not find module ‘IO.FFI’<br>
&gt;&nbsp; &nbsp; &nbsp;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&nbsp; -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!&nbsp; Note that I removed the "module XX where" 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; "/home/martin/adga2/agda-stadlib/src/" so that's what you should use<br>
&gt;&gt; for the -i option.<br>
&gt;&gt;<br>
&gt;&gt; The haskell library in "/home/martin/adga2/agda-stadlib/ffi/" 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 "module ag where" to "module Main where"<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&nbsp; <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&nbsp; directory<br>
&gt;&gt; &gt; /home/martin/adga2/agda-stadlib<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; cd&nbsp; ffi<br>
&gt;&gt; &gt; cabal install Setup.hs<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; does it mean that the&nbsp; extracted&nbsp; file path is the library&nbsp; 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't complain if it<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt; doesn'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 "Hello, Agda!")<br>
&gt;&gt; &gt;&gt; &gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt;<br>
&gt;&gt; &gt;&gt; &gt; &gt; I remove "module ag where" (because this module has `main' 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; "Hello, Agda!"<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 "import Foo",<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' 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' and `open'.<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></div></div>                                               </div></div></div>                                               </div></body>
</html>