<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div>Is it possible to run in interactive mode?<br>
<br>
<div class="acompli_signature">Sent from <a href="https://aka.ms/sdimjr">Outlook Mobile</a></div>
<br>
</div>
<br>
<br>
<br>
<div class="gmail_quote">On Tue, Dec 8, 2015 at 9:08 AM -0800, &quot;Sergei Meshveliani&quot;
<span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>
<br>
</div>
<div class="BodyFragment">
<div class="PlainText">On Tue, 2015-12-08 at 16:10 &#43;0800, Mandy Martino wrote:<br>
&gt; The interactive mode is no longer supported. Don't complain if it<br>
&gt; doesn't work.<br>
&gt; Main&gt; :l ag.agda<br>
&gt; Checking ag (/home/martin/adga2/ag.agda).<br>
&gt; /home/martin/adga2/ag.agda:3,13-25<br>
&gt; Failed to find source of module IO.Primitive in any of the<br>
&gt; following locations:<br>
&gt; /home/martin/adga2/IO/Primitive.agda<br>
&gt; /home/martin/adga2/IO/Primitive.lagda<br>
&gt; /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br>
&gt; /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda<br>
&gt; when scope checking the declaration<br>
&gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt; Failed.<br>
&gt; Main&gt;<br>
&gt; <br>
&gt; module ag where<br>
&gt; <br>
&gt; open import IO.Primitive using (IO; putStrLn)<br>
&gt; open import Data.String using (toCostring; String)<br>
&gt; open import Foreign.Haskell using (Unit)<br>
&gt; <br>
&gt; main : IO Unit<br>
&gt; main = putStrLn (toCostring &quot;Hello, Agda!&quot;)<br>
&gt; <br>
<br>
I remove&nbsp; &quot;module ag where&quot;&nbsp; (because this module has `main' in it),<br>
and apply<br>
<br>
&nbsp;&nbsp;&nbsp; agda -c $agdaLibOpt Hello.agda<br>
<br>
where&nbsp; $agdaLibOpt&nbsp; contains the path to the&nbsp; /src&nbsp; directory of<br>
Standard library.<br>
This makes the executable file&nbsp; Hello.<br>
Then, the command&nbsp; <br>
<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ./Hello&nbsp; <br>
prints&nbsp; <br>
&quot;Hello, Agda!&quot;<br>
<br>
<br>
&gt; why use open import, but not import<br>
<br>
After&nbsp; &quot;import Foo&quot;,<br>
<br>
one can write&nbsp; Foo.foo,&nbsp; if&nbsp; foo&nbsp; is defined in&nbsp; Foo&nbsp; module.<br>
After<br>
&nbsp; import Foo<br>
&nbsp; open Foo using (foo) <br>
<br>
one can write `foo' in the scope.<br>
And the line<br>
<br>
&nbsp; 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>
</div>
</div>
</body>
</html>