<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:·s²Ó©úÅé
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">actually </font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">i guess to run with</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">agda -I -c $stdlibpath </font></div><div><br>can this interactive mode using the standard library path ?<br><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> Subject: Re: [Agda] how to run helloworld in agda<br>> From: mechvel@botik.ru<br>> To: tesleft@hotmail.com<br>> CC: agda@lists.chalmers.se<br>> Date: Wed, 9 Dec 2015 16:02:34 +0400<br>> <br>> On Tue, 2015-12-08 at 23:48 +0000, Martin Mandy wrote:<br>> > Is it possible to run in interactive mode?<br>> > <br>> <br>> emacs Hello.agda<br>> <br>> Ctrl-C Ctrl-l<br>> <br>> <br>> This type-checks it.<br>> <br>> Then see http://wiki.portal.chalmers.se/agda/pmwiki.php<br>> <br>> and click at Quick Editing Guide.<br>> <br>> 1. I do not recall how to run it in interactive mode.<br>> 2. (Currently) most programs run interactively many times slower than a<br>> compiled program.<br>> 3. Before using "emacs Hello.agda" certain agda-mode needs to be<br>> added to the emacs editor.<br>> See<br>> https://github.com/agda/agda/blob/2.4.2/README.md<br>> <br>> Today I myself fail with this agda-mode of emacs, so that I run Agda<br>> only from the command line.<br>> <br>> ------<br>> Sergei <br>> <br>> <br>> <br>> <br>> > Sent from Outlook Mobile<br>> > <br>> > <br>> > <br>> > <br>> > <br>> > On Tue, Dec 8, 2015 at 9:08 AM -0800, "Sergei Meshveliani"<br>> > <mechvel@botik.ru> wrote:<br>> > <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>> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<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></div></div> </div></body>
</html>