[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

On 19 December 2015 at 03:23, Mandy Martino <tesleft at hotmail.com> wrote:
> time agda -c hello.agda -i. -iagda-stdlib/src/
> --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
>

You don't need `--ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs`
with the agda-stdlib library.


> open import IO
> main = putStrLn "Hello World"
>

The above program requires the agda-prelude library, but you are using
the agda-stdlib library.

> martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i.
> -iagda-stdlib/src/
> --ghc-flag=/home/martin/hilbertreborn/agda-stdlib/ffi/IO/FFI.hs
...
> (/home/martin/hilbertreborn/agda-stdlib/src/Data/Maybe/Base.agda).
>      Checking Data.Bool.Base
> (/home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda).
> /home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5-5
> /home/martin/hilbertreborn/agda-stdlib/src/Data/Bool/Base.agda:32,5: Parse
> error
> COMPILED_DATA_UHC<ERROR>
>  Bool __BOOL__ __TRUE__ __FALS...

Your version of agda-stdlib is not compatible with your version of Agda.

In http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
you can see which version of agda-stdlib is compatible with your
version of Agda.

-- 
Andrés