-
Notifications
You must be signed in to change notification settings - Fork 0
/
intro.tex
99 lines (88 loc) · 4.78 KB
/
intro.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
\paragraph{Note for CPP 2021 reviewers}
Running the examples in the tutorial requires the source code of Lassie, which
we have submitted as non-anonymous material. We chose to submit the tutorial
anonymously, as it can be read with having a HOL4 and Lassie session running
interactively.
Once the non-anonymous materials can be accessed, please put them in the directory \texttt{\$BASEDIR}
noted in the script and run the setup script from \autoref{sec:script}.
\section{Introduction/Setup}
%
As with any programming language, picking up an ITP system first requires
installing the system.
In this guide we use the HOL4~\cite{HOL4web} theorem prover.
The guide also uses a tool called \emph{Lassie}, equipping HOL4 with training
wheels.
To follow this guide, \texttt{polyML}, \texttt{Apache Ant}, and \texttt{ruby}
must be installed.
For \texttt{polyML}, we recommend downloading the latest version from git
(\url{https://github.com/polyml/polyml}).
Both \texttt{Apache Ant}, and \texttt{ruby} can be installed through the system
package manager on mainline Linux distributions.
On Mac OS they should be available through \texttt{brew}.
We provide a Debian setup script that makes sure all the dependencies are
installed,
and downloads and installs the latest versions of HOL4 and Lassie with this
guide (\autoref{sec:script}).
Running the setup script temporarily sets the variables \texttt{HOLDIR}, and
\texttt{LASSIEDIR} to the directories where HOL4 and Lassie have been installed.
To use both tools later, these variables must be be configured permanently
before running HOL4.
\subsection{Running HOL4}
We will explain how to interact using HOL4 using the emacs editor.
If you are not familiar with using emacs in general, we recommend the
built-in tutorial which is started by pressing \ekey{Control} together with
\ekey{h}, then \ekey{t}. An online version is available at
\url{https://www.gnu.org/software/emacs/tour/}.
There also exist plugins for interacting with HOL4 using the vim, and Sublime
text editors, and the overall interaction is the same, only the keybindings may
change.
When emacs is started, it normally tries to load a Lisp program from an
initialization file, or init file for short. This file, if it exists, specifies
how to initialize Emacs for you. Emacs looks for your init file using the
filenames \verb!~/.emacs!, \verb!~/.emacs.el!, and
\verb!~/.emacs.d/init.el!; you can choose to use any one of these three names.
Here, \verb!~/! stands for your home directory
(\url{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html}).
To interact with HOL4 within emacs, it suffices to append the following lines to
the emacs configuration file:
\begin{lstlisting}
(load-file "<HOL install dir>/tools/hol-unicode.el")
(load-file "<HOL install dir>/tools/hol-input.el")
(load-file "<HOL install dir>/tools/holscript-mode.el")
(load-file "<HOL install dir>/tools/hol-mode.el")
\end{lstlisting}
\noindent Here, \lstinline{<HOL install dir>} is the same path as the one
to which \texttt{HOLDIR} is set.
After loading the files, respectively restarting emacs, HOL4 files will by
default open in the HOL4 script mode.
In general, HOL4 files always end with the suffix \texttt{Script.sml}.
For example, a theory about natural numbers would be called
\texttt{naturalNumbersScript.sml}
In HOL4 speak, files ending with \texttt{Script.sml} are called \emph{script files}.
To interact with HOL4 we must first start a read-eval-print loop (REPL), similar
to interpreter of programming languages like ruby or python.
After opening a script file in emacs, HOL4 is started by presssing
first the \texttt{Alt} key together with \texttt{h}, then \texttt{H}.
In emacs this keybinding is abbreviated as \ekey{M-h H}, where \ekey{M} refers
to the \texttt{Alt} key\footnote{The \ekey{M} originates from the fact that
emacs users refer to the \ekey{Alt} key as \emph{Meta}.}.
After pressing the keybinding, emacs interactively prompts for a position of
the HOL4 REPL (the prompt reads \lstinline{HOL buffer position:}).
Possible options are \texttt{vertical}, \texttt{horizontal}, and
\texttt{new-frame}.
The first two split the current either vertically or horizontally to show the
HOL4 REPL.
Option \texttt{new-frame} will open the REPL in a separate window (as
\emph{frame} is ``emacs speak'' for windows).
For users with a single monitor, we recommend \texttt{horizontal}, and if two
or more monitors are available, \texttt{new-frame}.
A closing remark on using emacs:
If you ever find yourself stuck, pressing \ekey{C-g} (\ekey{Control} and
\ekey{g} at the same time) will abort any emacs process and get you back to
editing text, and pressing \ekey{M-h} {C-c} (\ekey{Alt} and \ekey{h} followed by
\ekey{Control} and \ekey{c}) aborts any running HOL4 REPL process that may have
diverged.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: