See the official user manual for the most up-to-date version of the information on this page.
A module exporting a function main : IO a can be compiled to a standalone executable.
A tiny example of this, which would be put in a file called "hello.agda":
module hello where open import IO main = run (putStrLn "Hello, World!")
This uses the IO module in the standard library.
To compile the above program you can either use the command-line using the flag --compile (or -c) or C-c C-x C-c from within Emacs. If you get the error message "Could not find module IO.FFI", you need to compile and install the IO.FFI module, which is used by the MAlonzo Compiler. To do so, cd into the directory ffi in the standard library's directory, and then run cabal install.
The Agda standard library provides two different IO monads. Primitive.agda contains a simple binding to Haskell's IO monad and a few related functions. This IO type is the type that the main function expects. IO.agda contains a coinductive deep embedding which is used to isolate possible non-termination into the run function. It is recommended not to use the Primitive IO type directly but rather the wrapper provided in IO.agda.