repl.tex

\section{Interacting with the HOL4 REPL}

The HOL4 REPL is an extended version of the polyML~\cite{polymlweb} REPL, and
behaves like the REPL's of other interpreted languages.
In general, it is recommend to first open a script file before starting
the REPL.

\textbf{Important setup note:}We strongly recommend opening a file
\texttt{tutorialScript.sml} in the folder \texttt{\$LASSIEDIR/examples}, to make
sure that the below code can be run easily.
This is done by either manually creating an empty file named \texttt{tutorialScript.sml} in \texttt{\$LASSIEDIR/examples}
and opening it with the toolbar buttons in emacs, or using \ekey{C-x C-f} (\ekey{Control} and \ekey{x}, then \ekey{Control} and \ekey{f})
to open it within emacs, by typing in the path.

We will explain in \autoref{sec:libraries} how the file should start to make its
contents reusable. For now we simply use it as a scratchpad.
The REPL is started by pressing \ekey{M-h H} (\ekey{Alt} and \ekey{h}, then \ekey{H}),
and HOL4 code is send to the REPL with the keybinding \ekey{M-h M-r}
(pressing \ekey{Alt} and \ekey{h}, then \ekey{Alt} and \ekey{r}).

For example, type
\begin{lstlisting}
  3 + 5;
\end{lstlisting}

anywhere in the currently openend script file.
Sending is then done by first highlighting the code with emacs using \ekey{C-space}.
Here, \ekey{C} stands for \ekey{Control}, so to start marking text, press
\ekey{Control} together with the \ekey{space} key.
The arrow keys are used for marking the code to be send to the REPL, and once it
has been completely selected, press \ekey{M-h M-r}.

The REPL should print:
\begin{lstlisting}[frame=single]
> 3+5;
val it = 8: int
\end{lstlisting}

All of the functionality of the polyML REPL, and in general, the Standard ML
basis library (see e.g. \url{https://smlfamily.github.io/Basis/} for a reference)
are available in the HOL4 REPL.
Thus HOL4 supports creating and manipulating lists, strings, options, and
simple I/O.

It is strongly recommended to type or copy the code snippets from this tutorial
into an actual script file and sending them to the REPL with the keybinding \ekey{M-h M-r}.
This makes sure that the code can be experimented with and commands that have
been entered are not lost in the limbo of the REPL printouts.

As a quick point of reference, \autoref{tbl:keybindings} gives a short,
executive summary of the most commonly used keybindings, taken from the
documentation of the HOL4 emacs mode (\url{https://hol-theorem-prover.org/hol-mode.html}).

\begin{table}
  \centering
\begin{tabular}{@{}cll@{}}
  \toprule
  Keybinding & \multicolumn{1}{c}{Effect} & \multicolumn{1}{c}{Remark}\\
  \midrule
  \ekey{M-h H} & Start a new HOL4 session & \\
  \ekey{M-h M-r} & Send marked text to REPL & \\
  \ekey{M-h g} & Start a new proof & Must be within a \texttt{Theorem}, \texttt{Proof} block\\
  \ekey{M-h e} & Applies a tactic & Marked SML code must have type `tactic`\\
  \ekey{M-h d} & Stop current interactive proof \\
  \bottomrule
\end{tabular}
  \caption{Most common HOL4-mode keybindings}\label{tbl:keybindings}
\end{table}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: