123456789101112131415161718192021222324252627282930313233343536373839 |
- == Using Alonzo ==
- agda --alonzo File.agda
- or
- agda -c File.agda
- produces File.hs
- compile it with
- ghc -c File.hs
- The main module should contain the function mainS : String, compile it with
- ghc --make -main-is File.main File.hs
- There is a shell script "almake" that will do both, provided you have
- compiled all dependencies beforehand.
- Prerequisites
- You need the following runtime files:
- RTS.hs RTN.hs RTP.hs
- RTN.agda RTP.agda
- NEVER run agda -c on RT* files as it will destroy the corresponding .hs files
- There is a "runtime" target in the Makefile, so running
- make runtime
- will compile the runtime files for you.
- There is a small prelude included, you can compile it with
- make prelude
|