tweak README

1 files changed, 50 insertions, 31 deletions

diff --git a/README b/README
index 30cebd99..a2c29c6b 100644
--- a/README
+++ b/README
@@ -2,44 +2,62 @@
 
 Guide to Sail, as of Feb 25, 2016. 
 
-Note: the repository name will change to sail for a public release
-
 ********************************************************************
 OVERVIEW
 
 This repository provides several tools relating to the Sail
-specification language. There is sail, the type checker and compiler
-for programs in the Sail language; a sequential Sail interpreter,
-which evaluates an Elf binary for an architecture that has been
-specified using Sail; an interface to the PPCMEM concurrent
-evaluation and exploration tool; and a formal definition of the Sail
-language and type system.
-
-There is an example Sail specification of a MIPS processor in the mips
-subdirectory, mips.sail
-
-To check the types of definitions within a specification, one uses the
-sail executable:
+specification language:
+
+- sail, the type checker and compiler for programs in the Sail
+  language;
+
+- an example Sail specification of a MIPS processor (in mips/mips.sail)
+
+- a sequential Sail interpreter, which evaluates an ELF binary for an
+  architecture that has been specified using Sail (for ABIs included
+  in our ELF specification);
+
+- machinery to interface with the PPCMEM concurrent evaluation
+  exploration tool; and
+
+- a formal definition of the Sail language and type system.
+
+- an emacs mode, including syntax highlighting
+
+There is also the beginnings of a manual, in manual.pdf.  This
+currently just describes the language syntax, type system, common
+library, and a few tips for sail development; it doesn't yet really
+explain the language.  We can answer questions either by mail or some
+google/skype chat.
+
+Elsewhere we have substantial IBM POWER and ARM Sail specifications
+which we can send by email.
+
+To get started, one probably wants to develop a new definition by
+analogy with the existing MIPS definition, using the sail executable
+just to check that it is type-correct. After building sail (as
+described below), this is done by:
+
 ./sail mips/mips.sail
 
-There is a first-draft manual describing the language, common library,
-and some tips for sail development in manual.pdf
 
-Once sufficient instructions have been represented in a
-specification,then it may become desirable to run an executable
-sequentially to debug the specification and begin testing. For this,
-there is the sequential sail interpreter, which evaluates the
-specification on an ELF file. At present, this will require
-conversations with Kathy Gray, as connections within the sail
-interpreter implementation to the architecture being simulated have
-not been factored out into external specification files.
+Once sufficient instructions have been represented in a specification,
+then one may also want to run executables sequentially, to debug the
+specification and begin testing. For this, there is the sequential
+sail interpreter, which evaluates the specification on an ELF file. At
+present, doing this for a new architecture will require conversation
+with Kathy Gray, as the connections within the sail interpreter
+implementation to the architecture being simulated have not been
+factored out into external specification files.
 
 Building the architecture for compilation to connect to the
 interpreter, one uses the sail executable:
+
 ./sail mips/mips.sail -lem_ast
+
 which will generate a mips.lem file in the current directory, which
-will be linked with the sail interpreter. (It is not recommended to
-read this file, as the output is a verbose representation of the sail AST.)
+will be linked with the sail interpreter (the output is a verbose
+representation of the sail AST).
 
 *** In progress. Does not work yet ***
 To generate Lem specifications for theorem proving, one uses the sail
@@ -58,7 +76,7 @@ SAIL COMPILER
 
 The Sail compiler requires OCaml; it is tested on version 4.02.3.
 
-Run make in the top level l2 directory; this will generate an executable
+Run "make" in the top level l2 directory; this will generate an executable
 called sail in this directory. 
 
 make clean will remove this executable as well as the build files in
@@ -67,14 +85,15 @@ subdirectories.
 SAIL INTERPRETER
 
 The Sail interpreter relies on external access to two external tools:
+
     Lem: a specification language that generates theorem prover code
     for HOL4, Isabelle, and Coq, and executable OCaml code from a
-    specification.
-    It is a publicly available Bitbucket repository
+    specification.  It is a publicly available Bitbucket repository
     https://bitbucket.org/Peter_Sewell/lem
+
     Linksem: a formal specification of ELF that includes the facility
-    to read in an ELF file and represent them in uniform ways. 
-    It is a private Bitbucket repository. 
+    to read in an ELF file and represent them in uniform ways.  It is
+    a private Bitbucket repository.
 
 The Sail build system expects to find these repositories in in the same
 directory as the l2 repository by default. This can be changed with