Updates

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 37 insertions, 20 deletions

diff --git a/README b/README
index 9cfad16..afb358d 100644
--- a/README
+++ b/README
@@ -2,8 +2,10 @@
 
 OVERVIEW:
 
-The Compcert verified compiler is a compiler for a large subset of the 
-C programming language that generates code for the PowerPC processor.
+The Compcert verified compiler is a compiler for a large subset of the
+C programming language that generates code for the PowerPC and ARM
+processors.
+
 The distinguishing feature of Compcert is that it has been formally
 verified using the Coq proof assistant: the generated assembly code is
 formally guaranteed to behave as prescribed by the semantics of the
@@ -16,29 +18,38 @@ purposes.
 
 COPYRIGHT:
 
-The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008
-Institut National de Recherche en Informatique et en Automatique (INRIA).
-It is distributed under the conditions stated in file LICENSE.
+The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007,
+2008, 2009 Institut National de Recherche en Informatique et en
+Automatique (INRIA).  It is distributed under the conditions stated in
+file LICENSE.
 
 
-PREREQUISITES:
+SUPPORTED PLATFORMS:
+
+- PowerPC / MacOS   [stable]
+    For Apple Macs running the MacOS 10.4 or 10.5 operating system.
+    Both PowerPC-based and Intel-based Macs are supported.
+    The PowerPC code generated by the Compcert compiler runs
+    natively at full speed on PowerPC-based Macs, and runs under
+    software emulation at reduced speed on Intel-based Macs.
 
-* A computer running the MacOS 10.4 or 10.5 operating system.
-  Both PowerPC-based and Intel-based Macs are supported.
-  The PowerPC code generated by the Compcert compiler runs
-  natively at full speed on PowerPC-based Macs, and runs under
-  software emulation at reduced speed on Intel-based Macs.
-  At least 1 Gb of RAM is required to build Compcert from sources.
+- PowerPC / Linux   [somewhat experimental]
+    For PowerPC machines running the Linux operating system.
 
-* The XCode development tools, as found on the installation DVDs
-  for MacOS 10.  Before proceeding, check that the "gcc", "as" and
-  "make" tools are installed and accessible in the search path.
+- ARM / Linux       [experimental]
+   For ARM machines running the Linux operating system.
 
-* The Coq proof assistant, version 8.1pl3 or 8.1pl2 or 8.1.
-  (8.1pl1 does not work.)  Coq is free software, available from 
-  http://coq.inria.fr/
 
-* The Caml functional language, version 3.09 or 3.10.
+PREREQUISITES:
+
+* The "gcc", "as" and "make" tools must be installed and accessible in
+  the search path.  For MacOS X, you can get them by installing the
+  XCode development tools, as found on the installation DVDs.
+
+* The Coq proof assistant, version 8.1pl3.
+  Coq is free software, available from http://coq.inria.fr/
+
+* The Caml functional language, version 3.10 or later.
   Caml is free software, available from http://caml.inria.fr/
 
 
@@ -46,7 +57,13 @@ INSTALLATION:
 
 1- Configure the system.  From the top directory, do:
 
-             ./configure
+             ./configure <target>
+
+where <target> is one of:
+
+            macosx           (PowerPC, MacOS X)
+            ppc-linux        (PowerPC, Linux)
+            arm-linux        (ARM, Linux)
 
 This generates the Makefile.config file in the top directory
 and prepares and configures the CIL library in the cil/ subdirectory.