[Agda] how to run helloworld in agda

[Mandy Martino]

actually 
i  guess to run with
agda -I  -c  $stdlibpath 
can this  interactive mode  using the standard  library  path ?

Regards,
Martin 

> Subject: Re: [Agda] how to run helloworld in agda
> From: mechvel at botik.ru
> To: tesleft at hotmail.com
> CC: agda at lists.chalmers.se
> Date: Wed, 9 Dec 2015 16:02:34 +0400
> 
> On Tue, 2015-12-08 at 23:48 +0000, Martin Mandy wrote:
> > Is it possible to run in interactive mode?
> > 
> 
>   emacs Hello.agda
> 
>   Ctrl-C Ctrl-l
> 
> 
> This type-checks it.
> 
> Then see  http://wiki.portal.chalmers.se/agda/pmwiki.php
> 
> and click at  Quick Editing Guide.
> 
> 1. I do not recall how to run it in interactive mode.
> 2. (Currently) most programs run interactively many times slower than a
> compiled program.
> 3. Before using  "emacs Hello.agda"   certain  agda-mode  needs to be
> added to the  emacs  editor.
> See
>       https://github.com/agda/agda/blob/2.4.2/README.md
> 
> Today I myself fail with this agda-mode of emacs, so that I run Agda
> only from the command line.
> 
> ------
> Sergei 
> 
> 
> 
> 
> > Sent from Outlook Mobile
> > 
> > 
> > 
> > 
> > 
> > On Tue, Dec 8, 2015 at 9:08 AM -0800, "Sergei Meshveliani"
> > <mechvel at botik.ru> wrote:
> > 
> > 
> > On Tue, 2015-12-08 at 16:10 +0800, Mandy Martino wrote:
> > > The interactive mode is no longer supported. Don't complain if it
> > > doesn't work.
> > > Main> :l ag.agda
> > > Checking ag (/home/martin/adga2/ag.agda).
> > > /home/martin/adga2/ag.agda:3,13-25
> > > Failed to find source of module IO.Primitive in any of the
> > > following locations:
> > > /home/martin/adga2/IO/Primitive.agda
> > > /home/martin/adga2/IO/Primitive.lagda
> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.agda
> > > /home/martin/.cabal/share/i386-linux-ghc-7.10.1/Agda-2.4.2.3/lib/prim/IO/Primitive.lagda
> > > when scope checking the declaration
> > > open import IO.Primitive using (IO; putStrLn)
> > > Failed.
> > > Main>
> > > 
> > > module ag where
> > > 
> > > open import IO.Primitive using (IO; putStrLn)
> > > open import Data.String using (toCostring; String)
> > > open import Foreign.Haskell using (Unit)
> > > 
> > > main : IO Unit
> > > main = putStrLn (toCostring "Hello, Agda!")
> > > 
> > 
> > I remove  "module ag where"  (because this module has `main' in it),
> > and apply
> > 
> >     agda -c $agdaLibOpt Hello.agda
> > 
> > where  $agdaLibOpt  contains the path to the  /src  directory of
> > Standard library.
> > This makes the executable file  Hello.
> > Then, the command  
> > 
> >        ./Hello  
> > prints  
> > "Hello, Agda!"
> > 
> > 
> > > why use open import, but not import
> > 
> > After  "import Foo",
> > 
> > one can write  Foo.foo,  if  foo  is defined in  Foo  module.
> > After
> >   import Foo
> >   open Foo using (foo) 
> > 
> > one can write `foo' in the scope.
> > And the line
> > 
> >   open import Foo using (foo)
> > 
> > combines the above lines of `import' and `open'.
> > 
> > Regards,
> > 
> > ------
> > Sergei
> > 
> > 
> > 
> > 
> 
> 
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151209/a3c719ae/attachment.html