agda --compile --compile-dir <DIR> --ghc-flag "<GHC FLAGS>" <FILE>.agda

Compiles <FILE>.agda and hereditarily imported agda files to Haskell and to an executable.

Haskell files are written under the directory <DIR>/MAlonzo. If --compile-dir <DIR> is omitted, the current directory is used instead. Agda module A.B.C translates to Haskell module MAlonzo.A.B.C (to avoid conflicts between Agda and Haskell standard libraries.)

Those Haskell files are then automatically compiled to object files and an executable by the command

 ghc <GHC FLAGS> -i<DIR> -main-is MAlonzo.<FILE> <DIR>/Malonzo/<FILE>.hs --make

It is assumed that <FILE>.agda contains a definition of main :: IO a. If it does not, ghc finishes with an error, but never mind. The executable is <DIR>/MAlonzo/<FILE>(.exe), or whatever you specify via <GHC FLAGS>.

You can use IO from the standard library if you want to do some input/output.

Page last modified on October 12, 2018, at 09:11 pm
Powered by PmWiki