[Agda] how to run helloworld in agda

[Sergei Meshveliani]

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
> 
> 
> 
>