Restore manual.tex, accidentally deleted

Minor updates to README, still in progress

2 files changed, 11 insertions, 103 deletions

diff --git a/README b/README
index b02fce6d..fbc0fc4b 100644
--- a/README
+++ b/README
@@ -13,6 +13,8 @@ specification language:
 
 - a Sail specification of a MIPS ISA (in mips/)
 
+- a Sail specification of a Cheri ISA (in cheri/)
+
 - a Sail specification of part of the ARMv8 ISA (in arm/)
 
 - a sequential Sail interpreter, which evaluates an ELF binary for an
@@ -52,9 +54,9 @@ 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.
+with Robert Norton Wright or 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:
@@ -65,7 +67,6 @@ which will generate a mips.lem file in the current directory, which
 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
 executable with flag:
 ./sail mips/mips.sail -lem
@@ -83,7 +84,7 @@ SAIL COMPILER
 The Sail compiler requires OCaml; it is tested on version 4.02.3.
 
 Run "make" in the top level sail directory; this will generate an executable
-called sail in this directory. 
+called sail in this directory and will compile the interpreter files. 
 
 make clean will remove this executable as well as the build files in
 subdirectories.
@@ -102,7 +103,7 @@ The Sail interpreter relies on external access to two external tools:
     a public Bitbucket repository
     https://bitbucket.org/Peter_Sewell/linksem
 
-The Sail build system expects to find these repositories in in the same
+The Sail build system expects to find these repositories in the same
 directory as the sail repository by default. This can be changed with
 make variables LEM, LEMLIBOCAML, and ELFDIR
 
@@ -162,8 +163,8 @@ Will generate the files spec.lem and spec.ml in the current directory
 It is not recommended to try to read the generated Lem ast file, as it is a very verbose
 representation of the AST. 
 
-IN PROGRESS COMMANDS: -lem -ocaml
-The resulting output of these commands may well be untype checkable Lem or OCaml
+IN PROGRESS COMMANDS: -ocaml
+The resulting output of these commands may well be untype checkable OCaml
 
 
 ******************************************************************************
@@ -176,6 +177,7 @@ Top level directories
 src/            ML implementation of Sail frontend, Sail executable, subdirectories
 language/       Ott definitions of source language, pdfs as well
 mips/           Sail definition of a MIPS specification
+cheri/          Sail definition of a Cheri specification
 risc-v/         abandoned very partial attempt at RISC V specification
 l3-to-l2/       abandoned but not GC-ed directory
 
@@ -184,6 +186,7 @@ l2_parse.ott    Grammar of Sail generated by parser, superset of source language
 l2.ott          Grammar of Sail source
 l2_typ.ott      Grammar of Internal structures used for type annotations
 l2_rules.ott    Rules for type system
+manual.tex      Source of manual
 
 Relevant make commands:
 make          Builds pdfs for l2 and l2_parse, ml and lem files of grammars
diff --git a/language/manual.tex b/language/manual.tex
index 86aaa8b0..5d4b9d6a 100644
--- a/language/manual.tex
+++ b/language/manual.tex
@@ -17,101 +17,6 @@
 
 \newpage
 
-\section{Introduction}
-
-This is a manual describing the Sail specification language, its
-common library, compiler, interpreter and type system. However it is
-currently in early stages of being written, so questions to the
-developers are highly encouraged.
-
-\section{Tips for Writing Sail specifications}
-
-This section attempts to offer advice for writing Sail specifications
-that will work well with the Sail executable interpreter and
-compilers.
-
-These tips use ideomatic Sail code; the Sail syntax is formally
-defined in following section.
-
-Some tips might also be advice for good ways to specify instructions;
-this will come from a combination of users and Sail developers.
-
-\begin{itemize}
-
-\item Declare memory access functions as one read, one write announce,
-  and one write value for each kind of access.
-
-For basic user-mode instructions, there should be the need for only
-one memory read and two memory write function. These should each be
-declared using {\tt val extern} and should have effect {\tt wmem} and
-{\tt rmem} accordingly. 
-
-Commonly, a memory read function will take as parameters a size (an
-number below 32) and an address and return a bit vector with length (8
-* size). The sequential and concurrent interpreters both only read and
-write memory as a factor of bytes.
-
-\item Declare a default vector order
-
-Vectors can be either decreasing or increasing, i.e. if we have a
-vector \emph{a} with elements [1,2,3] then in an increasing specification the 1 is accessed
-with {\tt a[0]} but with {\tt a[2]} in a decreasing system. Early in
-your specification, it is beneficial to clarity to say default Ord inc
-or default Ord dec.
-
-\item Vectors don't necessarily begin indexing at 0 or n-1
-
-Without any additional specification, a vector will begin indexing at
-0 in an increasing spec and n-1 in a decreasing specification. A type
-declaration can reset this first position to any number. 
-
-Importantly, taking a slice of a vector does not reset the indexes. So
-if {\tt a = [1,2,3,4]} in an increasing system the slice {\tt a[2
-  ..3]} generates the vector {\tt [3,4]} and the 3 is indexed at 2 in either vector.
-
-\item Be precise in numeric types. 
-
-While Sail includes very wide types like int and nat, consider that
-for bounds checking, numeric operations, and and clear understanding,
-these really are unbounded quantities. If you know that a number in
-the specification will range only between 0 and 32, 0 and 4, $-32$ to
-32, it is better to use a specific range type such as $[|32|]$. 
-
-Similarly, if you don't know the range precisely, it may also be best
-to remain polymorphic and let Sail's type resolution work out bounds
-in a particular use rather than removing all bounds; to do this, use
-[:'n:] to say that it will polymorphically take some number.
-
-\item Use bit vectors for registers.
-
-Sail the language will readily allow a register to store a value of
-any type. However, the Sail executable interpreter expects that it is
-simulating a uni-processor machine where all registers are bit
-vectors.
-
-A vector of length one, such as \emph{a} can read the element of \emph{a}
-either with {\tt a} or {\tt a[0]}.
-
-\item Have functions named decode and execute to evaluate
-  instructions.
-
-The sail interpreter is hard-wired to look for functions with these names.
-
-\item Type annotations are necessary to read the contents of a
-  register into a local variable.
-
-The code {\tt x := GPR[4]}, where GPR is a vector of general purpose
-registers, will store a local reference to the fourth general purpose
-register, not the contents of that registe, i.e. this will not read
-the register. To read the register contents into a local variable, the
-type is required explicitly so {\tt (bit[64]) x := GPR[4]} reads the
-register contents into x. The type annotation may be on either side of
-the assignment.
-
-\end{itemize}
-
-
-
 \section{Sail syntax}
 
 \ottgrammartabular{