From 2c81fff611c458fe04b2de2045247bdc77f8f80a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 21 Jan 2019 19:02:46 +0000
Subject: Update manual snapshot and add basic sail -latex documentation

---
 doc/usage.tex | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 63 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/usage.tex b/doc/usage.tex
index d4f87393..2711fff5 100644
--- a/doc/usage.tex
+++ b/doc/usage.tex
@@ -147,7 +147,7 @@ files.
   call the \ll{cycle_count} function for this to work.
 \end{itemize}
 
-\subsection{Lem and Isabelle}
+\subsection{Lem, Isabelle \& HOL4}
 
 We have a separate document detailing how to generate Isabelle
 theories from Sail models, and how to work with those models in
@@ -191,6 +191,68 @@ mode, a list of commands can be accessed by typing \verb+:commands+,
 while \verb+:help+ can be used to provide some documentation for each
 command.
 
+\subsection{\LaTeX\ Generation}
+
+Sail can be used to generate latex for inclusion in documentation as:
+\begin{verbatim}
+sail -o DIRECTORY -latex FILES
+\end{verbatim}
+The list of \verb+FILES+ is a list of Sail files to produce latex for,
+and \verb+DIRECTORY+ is the directory where the generated latex will
+be placed. The list of files must be a valid type-checkable series of
+Sail files. The intention behind this latex generation is for it to be
+included within existing ISA manuals written in Latex, as such the
+latex output generates a list of commands for each top-level Sail
+declaration in \verb+DIRECTORY/commands.tex+. The rest of this section
+discusses the stable features of the latex generation process---there
+are additional features for including markdown doc-comments in Sail
+code and formatting them into latex for inclusion id documentation,
+among other things, but these features are not completely stable
+yet. This manual itself makes use of the Sail latex generation, so
+\verb+doc/manual.tex+, and \verb+doc/Makefile+ can be used to see how
+the process is set up.
+
+
+\paragraph{Requirements} The generated latex uses the \emph{listings} package for formatting
+source code, uses the macros in the \emph{etoolbox} package for the
+generated commands, and relies on the \emph{hyperref} package for
+cross-referencing. These packages are available in most TeX
+distributions, and are available as part of thetexlive packages for
+Ubuntu.
+
+\paragraph{Usage} Due to the oddities of latex verbatim environments each Sail
+declaration must be placed in it's own file then the command in
+\verb+commands.tex+ includes in with \verb+\lstinputlisting+. To
+include the generated Sail in a document one would do something like:
+\begin{lstlisting}[language=TeX]
+  \input{commands.tex}
+  \sailval{my_function}
+  \sailfn{my_function}
+\end{lstlisting}
+which would enclude the type declaration (\verb+\sailval+) for
+\verb+my_function+ as well as type body of that function
+(\verb+\sailfn+).
+
+It is sometimes useful to include multiple versions of the same Sail
+definitions in a latex document. In this case the \verb+-latex_prefix+
+option can be used. For example if we used \verb+-latex_prefix prefix+
+then the above example would become:
+\begin{lstlisting}[language=TeX]
+  \input{commands.tex}
+  \prefixval{my_function}
+  \prefixfn{my_function}
+\end{lstlisting}
+
+The generated definitions are created wrapped in customisable macros
+that can be overridden to change the formatting of the Sail code. For
+\verb+\sailfn+ there is a macro \verb+\saildocfn+ that must be defined,
+and similarly for the other Sail toplevel types.
+
+\paragraph{Cross-referencing} For each macro \verb+\sail+\emph{X}\verb+{id}+ there is a macro
+\verb+\sailref+\emph{X}\verb+{id}{text}+ which creates a
+hyper-reference to the original definition. This requires the
+hyper-ref package.
+
 \subsection{Other options}
 
 Here we summarize most of the other options available for
-- 
cgit v1.2.3