<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">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 find the path of stdlib after it install ?</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><div>martin@ubuntu:~/adga2/stdlib/agda-stdlib/ffi$ cat Setup.hs </div><div>import Distribution.Simple</div><div><br></div><div>main = defaultMain</div><div style="font-size: 12pt;"><br></div></font><div>martin@ubuntu:~/adga2/stdlib/agda-stdlib$ ls</div><div>agda-stdlib.agda-lib GenerateEverything.hs LICENCE README.md</div><div>AllNonAsciiChars.hs GNUmakefile notes Setup.hs</div><div>CHANGELOG Header publish-listings.sh src</div><div>doc index.sh README</div><div>ffi lib.cabal README.agda</div><div><br></div><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: 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>> > /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></div></div> </div></body>
</html>