[Agda] how to run helloworld in agda

[Mandy Martino]

Hi  Andres,
i  use  only  one line  import  Algebra and then compile  got  error
martin at ubuntu:~/hilbertreborn$ cat hello.agdaopen import Algebramartin at ubuntu:~/hilbertreborn$
martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib-0.11/src --ghc-flag=/home/martin/hilbertreborn/agda-stdlib-0.11/ffi/Data/FFI.hs
/home/martin/hilbertreborn/MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hsCompiling Relation.Nullary in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Nullary.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Nullary.hsCompiling hello in /home/martin/hilbertreborn/hello.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hsCalling: ghc -O -o /home/martin/hilbertreborn/hello -Werror /home/martin/hilbertreborn/agda-stdlib-0.11/ffi/Data/FFI.hs -i/home/martin/hilbertreborn -main-is MAlonzo.Code.Qhello /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patternsCompilation error:
MAlonzo/Code/Agda/Primitive.hs:4:18:    Could not find module `Agda.FFI'    Use -v to see a list of the files searched for.

real	0m9.028suser	0m6.140ssys	0m1.436s

Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 05:29:42 -0500
> Subject: Re: [Agda] how to run helloworld in agda
> To: tesleft at hotmail.com
> CC: leo at halfaya.org; ulf.norell at gmail.com; agda at lists.chalmers.se
> 
> On 19 December 2015 at 05:11, Mandy Martino <tesleft at hotmail.com> wrote:
> > how to uninstall  this  incompatible  version?
> 
> There is no command for uninstalling the agda-stdlib library. You can
> delete the agda-stdlib directory or you can use a different directory
> for a different version of the agda-stdlib library.
> 
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/dc570592/attachment-0001.html