ITP-Course/lectures/05_usage.tex

\part{Basic HOL Usage}

\frame[plain]{\partpage}

\begin{frame}
\frametitle{HOL Technical Usage Issues}
\begin{itemize}
\item practical issues are discussed in practical sessions
\begin{itemize}
\item how to install HOL
\item which key-combinations to use in emacs-mode
\item detailed signature of libraries and theories
\item all parameters and options of certain tools
\item \ldots
\end{itemize}
\item exercise sheets sometimes
\begin{itemize}
\item ask to read some documentation
\item provide examples
\item list references where to get additional information
\end{itemize}
\item if you have problems, ask me outside lecture (\href{mailto:thomas@tuerk-brechen.de}{thomas@tuerk-brechen.de})
\item covered only very briefly in lectures
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Installing HOL}
\begin{itemize}
\item webpage: \url{https://hol-theorem-prover.org}
\item HOL supports two SML implementations
\begin{itemize}
\item Moscow ML (\url{http://mosml.org})
\item \alert{PolyML} (\url{http://www.polyml.org})
\end{itemize}
\item I recommend using PolyML
\item please use emacs with
\begin{itemize}
\item hol-mode
\item sml-mode
\item hol-unicode, if you want to type Unicode 
\end{itemize}
\item please install recent revision from git repo or Kananaskis 11 release
\item documentation found on HOL webpage and with sources
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{General Architecture}
\begin{itemize}
\item HOL is a collection of SML modules
\item starting HOL starts a SML Read-Eval-Print-Loop (REPL) with
\begin{itemize}
\item some HOL modules loaded
\item some default modules opened
\item an input wrapper to help parsing terms called \texttt{unquote}
\end{itemize}
\item \texttt{unquote} provides special quotes for terms and types
\begin{itemize}
\item implemented as input filter
\item \hol{``my-term``\ } becomes \ml{Parse.Term [QUOTE "my-term"]}
\item \hol{``:my-type``} becomes \ml{Parse.Type [QUOTE ":my-type"]}
\end{itemize}
\item main interfaces
\begin{itemize}
\item \emph{emacs} (used in the course)
\item vim
\item bare shell
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Filenames}
\begin{itemize}
\item \emph{\texttt{*Script.sml}} --- HOL proof script file 
\begin{itemize}
\item script files contain definitions and proof scripts
\item executing them results in HOL searching and checking proofs
\item this might take very long
\item resulting theorems are stored in \texttt{*Theory.\{sml|sig\}} files
\end{itemize}
\item \emph{\texttt{*Theory.\{sml|sig\}}} --- HOL theory\\
\begin{itemize}
\item auto-generated by corresponding script file
\item load quickly, because they don't search/check proofs
\item do not edit theory files
\end{itemize}
\item \emph{\texttt{*Syntax.\{sml|sig\}}} --- syntax libraries \\
\begin{itemize}
\item contain syntax related functions 
\item \ie functions to construct and destruct terms and types
\end{itemize}
\item \emph{\texttt{*Lib.\{sml|sig\}}} --- general libraries
\item \emph{\texttt{*Simps.\{sml|sig\}}} --- simplifications
\item \emph{\texttt{selftest.sml}} --- selftest for current directory
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Directory Structure}
\begin{itemize}
\item \emph{\texttt{bin}} --- HOL binaries 
\item \emph{\texttt{src}} --- HOL sources
\item \emph{\texttt{examples}} --- HOL examples
\begin{itemize}
\item interesting projects by various people
\item examples owned by their developer
\item coding style and level of maintenance differ a lot
\end{itemize}
\item \emph{\texttt{help}} --- sources for reference manual
\begin{itemize}
\item after compilation home of reference HTML page
\end{itemize}
\item \emph{\texttt{Manual}} --- HOL manuals
\begin{itemize}
\item Tutorial
\item Description
\item Reference (PDF version)
\item Interaction
\item Quick (cheat pages)
\item Style-guide
\item \ldots
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Unicode}
\begin{itemize}
\item HOL supports both Unicode and pure ASCII input and output
\item advantages of Unicode compared to ASCII
\begin{itemize}
\item easier to read (good fonts provided)
\item no need to learn special ASCII syntax
\end{itemize}
\item disadvanges of Unicode compared to ASCII
\begin{itemize}
\item harder to type (even with \texttt{hol-unicode.el})
\item less portable between systems
\end{itemize}
\item whether you like Unicode is highly a matter of personal taste
\item HOL's policy
\begin{itemize}
\item no Unicode in HOL's source directory \texttt{src}
\item Unicode in examples directory \texttt{examples} is fine
\end{itemize}
\item I recommend turning Unicode output off initially
\begin{itemize}
\item this simplifies learning the ASCII syntax
\item no need for special fonts
\item it is easier to copy and paste terms from HOL's output
\end{itemize}
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Where to find help?}
\begin{itemize}
\item reference manual
\begin{itemize}
\item available as HTML pages, single PDF file and in-system help
\end{itemize}
\item description manual
\item Style-guide (still under development)
\item HOL webpage (\url{https://hol-theorem-prover.org})
\item mailing-list \texttt{hol-info}
\item \ml{DB.match} and \ml{DB.find}
\item \ml{*Theory.sig} and \ml{selftest.sml} files
\item ask someone, \eg me :-) (\href{mailto:thomas@tuerk-brechen.de}{thomas@tuerk-brechen.de})
\end{itemize}
\end{frame}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End: