← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/Alonzo/README

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/Alonzo/README
1
 
== Using Alonzo == 
2
 
 
3
 
agda --alonzo File.agda
4
 
 
5
 
or
6
 
 
7
 
agda -c File.agda
8
 
 
9
 
produces File.hs
10
 
 
11
 
compile it with
12
 
ghc -c File.hs
13
 
 
14
 
The main module should contain the function mainS : String, compile it with
15
 
 
16
 
ghc --make -main-is File.main File.hs
17
 
 
18
 
There is a shell script "almake" that will do both, provided you have
19
 
compiled all dependencies beforehand.
20
 
 
21
 
Prerequisites
22
 
 
23
 
You need the following runtime files:
24
 
 
25
 
RTS.hs RTN.hs RTP.hs
26
 
RTN.agda RTP.agda
27
 
 
28
 
NEVER run agda -c on RT* files as it will destroy the corresponding .hs files
29
 
 
30
 
There is a "runtime" target in the Makefile, so running 
31
 
 
32
 
make runtime
33
 
 
34
 
will compile the runtime files for you.
35
 
 
36
 
There is a small prelude included, you can compile it with
37
 
 
38
 
make prelude