From 13848ba495e79fcc6efe10cf7d98f68fa9453f29 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 11 May 2018 17:23:36 +0100
Subject: Add link to Thomas's Sail/Isabelle documentation in manual

Replace the old manual with new version in repository root
---
 doc/manual.tex |  2 +-
 doc/types.tex  |  2 ++
 doc/usage.tex  | 42 +++++++++++++++++++++++++++++++++---------
 3 files changed, 36 insertions(+), 10 deletions(-)

(limited to 'doc')

diff --git a/doc/manual.tex b/doc/manual.tex
index 1148835e..1645f735 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -65,7 +65,7 @@
 \title{The Sail instruction-set semantics specification language}
 
 \author{Kathryn E. Gray \and Peter Sewell \and Christopher Pulte \and
-  Shaked Flur \and Robert Norton-Wright \and Alasdair Armstrong}
+  Shaked Flur \and Robert Norton-Wright \and Alasdair Armstrong \and Thomas Bauereiss}
 
 \maketitle
 
diff --git a/doc/types.tex b/doc/types.tex
index 11037c91..a74cdea9 100644
--- a/doc/types.tex
+++ b/doc/types.tex
@@ -1,6 +1,8 @@
 \section{Type System}
 \label{sec:types}
 
+(This section is still a work in progress)
+
 \newcommand{\tcheck}[3]{#1 \vdash #2 \Leftarrow #3}
 \newcommand{\tinfer}[3]{#1 \vdash #2 \Rightarrow #3}
 \newcommand{\msail}[1]{\text{\lstinline[mathescape]+#1+}}
diff --git a/doc/usage.tex b/doc/usage.tex
index 293d0587..3b8eed5f 100644
--- a/doc/usage.tex
+++ b/doc/usage.tex
@@ -38,7 +38,7 @@ AST is parsed~\footnote{This can affect precedence declarations for custom user
 
 \subsection{OCaml compilation}
 
-To compile a sail specification into OCaml, one calls Sail as
+To compile a Sail specification into OCaml, one calls Sail as
 \begin{verbatim}
 sail -ocaml FILES
 \end{verbatim}
@@ -76,25 +76,46 @@ specification. In particular \verb+elf.sail+ defines a function
 correct location. ELF loading is done by the linksem
 library\footnote{\url{https://github.com/rems-project/linksem}}.
 
-There is also an \verb+-ocaml_trace+ option which instruments the
-generated OCaml code with tracing information this option implies \verb+-ocaml+.
+There is also an \verb+-ocaml_trace+ option which is the same as
+\verb+-ocaml+ except it instruments the generated OCaml code with
+tracing information.
 
-\subsection{C compilation}
+%% \subsection{C compilation}
 
-WIP but basically like OCaml
+%% WIP but basically like OCaml
 
-\subsection{Lem embedding}
+\subsection{Lem and Isabelle}
 
-\TODO{Document generating lem}
+We have a separate document detailing how to generate Isabelle
+theories from Sail models, and how to work with those models in
+Isabelle, see:
+\begin{center}
+\url{https://github.com/rems-project/sail/raw/sail2/snapshots/isabelle/Manual.pdf}
+\end{center}
+Currently there are generated Isabelle snapshots for some of our
+models in \verb+snapshots/isabelle+ in the Sail repository. These
+snapshots are provided for convenience, and are not guaranteed to be
+up-to-date.
+
+In order to open a theory of one of the specifications in Isabelle,
+use the -l Sail command-line flag to load the session containing the
+Sail library. Snapshots of the Sail and Lem libraries are in the
+\verb+lib/sail+ and \verb+lib/lem+ directories, respectively. You can
+tell Isabelle where to find them using the -d flag, as in
+\begin{verbatim}
+isabelle jedit -l Sail -d lib/lem -d lib/sail riscv/Riscv.thy
+\end{verbatim}
+When run from the \verb+snapshots/isabelle+ directory this will open
+the RISC-V specification.
 
 \subsection{Interactive mode}
 
-Compiling sail with
+Compiling Sail with
 \begin{verbatim}
 make isail
 \end{verbatim}
 builds it with a GHCi-style interactive interpreter. This can be used
-by starting Sail with \verb+sail -i+. If sail is not compiled with
+by starting Sail with \verb+sail -i+. If Sail is not compiled with
 interactive support the \verb+-i+ flag does nothing. Sail will still
 handle any other command line arguments as per usual, including
 compiling to OCaml or Lem. One can also pass a list of commands to the
@@ -127,6 +148,9 @@ indicated by starting with the letter d.
   improve typechecking times if you are repeatedly typechecking the
   same specification while developing it.
 
+\item \verb+-no_lexp_bounds_check+ Turn off bounds checking in the left
+  hand side of assignments.
+
 \item \verb+-no_effects+ Turn off effect checking. May break some
   backends that assume effects are properly checked.
 
-- 
cgit v1.2.3