[Agda] how to run helloworld in agda

[Martin Mandy]

Is it possible to run in interactive mode?

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/20151208/50d67c69/attachment.html