<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">after untar </font><a href="https://agda.github.io/agda-stdlib" target="_blank">https://agda.github.io/agda-stdlib</a><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">into directory </font></div><div><font size="3" style="font-size:12pt;" color="#000000">/home/martin/adga2/agda-stadlib</font></div><div><br></div><div>cd ffi</div><div>cabal install Setup.hs</div><div><br>does it mean that the extracted file path is the library path ?</div><div><br></div><div>/home/martin/adga2/agda-stadlib ?<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 15:41:17 +0400<br>> <br>> On Wed, 2015-12-09 at 19:11 +0800, Mandy Martino wrote:<br>> > Hi,<br>> > <br>> > <br>> > how to find the path of stdlib after it install ?<br>> > <br>> <br>> For example, I have installed Standard library in <br>> <br>> /home/mechvel/agda/stLib/oct29-2015/src,<br>> <br>> so that this directory contains Algebra.agda, and other .agda files and<br>> subdirectories. <br>> Agda is called as <br>> <br>> agda -c $agdaLibOpt MyProgram.agda<br>> <br>> where $agdaLibOpt is<br>> <br>> -i . -i /home/mechvel/agda/stLib/oct29-2015/src -i /home/mechvel/source<br>> <br>> It lists 3 paths. The last path points to where reside my .agda files<br>> which MyProgram imports. <br>> <br>> ------<br>> Sergei<br>> <br>> <br>> > martin@ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs <br>> > import Distribution.Simple<br>> > <br>> > <br>> > main = defaultMain<br>> > <br>> > <br>> > martin@ubuntu:~/adga2/stdlib/agda-stdlib$ ls<br>> > agda-stdlib.agda-lib GenerateEverything.hs LICENCE<br>> > README.md<br>> > AllNonAsciiChars.hs GNUmakefile notes<br>> > Setup.hs<br>> > CHANGELOG Header publish-listings.sh src<br>> > doc index.sh README<br>> > ffi lib.cabal README.agda<br>> > <br>> > <br>> > <br>> > Regards,<br>> > <br>> > <br>> > Martin <br>> > <br>> > <br>> > > 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: Tue, 8 Dec 2015 21:06:16 +0400<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>> > ><br>> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda<br>> > ><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>