[Agda] compiling Hello.agda

[James Deikun]

On Wed, 2012-07-18 at 22:11 +0400, Serge D. Mechveliani wrote:
>  agda -c -i /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1 Hello.agda
>  
> It reports
> -------- 
> the name of the top level module does not match the file name. The
> module Hello should be defined in one of the following files:
>   /home/mechvel./cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1/Hello.agda
>   /home/mechvel./cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1/Hello.lagda

You need, in addition, the option '-i .'.  This may or may not solve all
your problems, but it should solve the above error.