diff options
Diffstat (limited to 'doc/usage.tex')
| -rw-r--r-- | doc/usage.tex | 64 |
1 files changed, 63 insertions, 1 deletions
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 |