[Agda] compiling Hello.agda

[Serge D. Mechveliani]

People,
I am trying to run Agda for the first time, and need help with this.
I have 
 * ghc-7.4.1     working,  
 * Cabal         installed in  /home/mechvel./cabal,
 * Agda-2.3.0.1  made from source and installed in
                                      /home/mechvel/.cabal/bin,
 * The  Agda Standard Library, version 0.6,
   made from source and installed in 
             /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1,

 * /home/mechvel/.cabal/bin  included in  $path

-- all these are in my user home directory. 
 
In  Chapter 4  of  tutorial.pdf  
"Dependently Typed Programming in Agda",  I find (in Chapter 4.3)
the program
    main : IO Unit
    main = putStrLn "Hello, world!" 

I understand this tutorial so that one need to prefix this source
with certain declarations for the types Unit and IO, with import from 
Haskell, and with certain pragmas -- as it is said in the
Chapters 4.1 -- 4.3.  So, the whole program must be

------------------------------------------------- Hello.agda ----
module Hello where

data Unit : Set where
 unit : Unit

{-# COMPILED_DATA Unit () () #-}

postulate IO : Set -> Set 

{-# COMPILED_TYPE IO IO #-}

open import Data.String 
postulate
  putStrLn : String -> IO Unit

{-# COMPILED putStrLn putStrLn #-}

main : IO Unit
main = putStrLn "hello!"
------------------------------------------------------------------

Is this so?

I put this file to  $myProjectRoot  and command there
(in Debian Linux, tcshell)

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

By  -i /home/mechvel.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1
I try to specify the directory of the Standard library installation.

README.agda  of the Standard Library writes
-- To make use of the library, add the path to the library's root
-- directory (src) to the Agda search path, either using the
-- --include-path flag or [..]

And where is the "Agda search path" ?
Is it            /home/mechvel/.cabal/bin  ?
I tried 
        agda -c -i /home/mechvel/haskell/agda/lib-0.6/src Hello.agda

-- with a similar effect.
Please, how to compile and run the above program?

Thank you in advance for help,

------
Sergei
mechvel at botik.ru