isabelle.tex 3.2 KB
Newer Older
1 2
\section{Isabelle/HOL}
\label{sec:isabelle}
MARCHE Claude's avatar
MARCHE Claude committed
3

4 5
\index{Isabelle proof assistant}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
6
When using Isabelle from \why, files generated from \why theories and
7 8 9
goals are stored in a dedicated XML format. Those files should not be
edited. Instead, the proofs must be completed in a file with the same
name and extension \texttt{.thy}. This is the file that is opened when
10
using ``Edit'' action in \texttt{why3 ide}.
11

12 13
\subsection{Installation}

Stefan Berghofer's avatar
Stefan Berghofer committed
14 15 16
You need version Isabelle2017 or Isabelle2018. Former versions are not
supported. We assume below that your version is 2018, please replace
2018 by 2017 otherwise.
17

Guillaume Melquiond's avatar
Guillaume Melquiond committed
18 19
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
20 21 22
\begin{verbatim}
<Why3 lib dir>/isabelle
\end{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
23
into either the user file
24
\begin{verbatim}
Stefan Berghofer's avatar
Stefan Berghofer committed
25
.isabelle/Isabelle2018/etc/components
26
\end{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
27
or the system-wide file
28 29 30
\begin{verbatim}
<Isabelle install dir>/etc/components
\end{verbatim}
31 32

\subsection{Usage}
33

Guillaume Melquiond's avatar
Guillaume Melquiond committed
34
The most convenient way to call Isabelle for discharging a \why goal
35
is to start the Isabelle/jedit interface in server mode. In this mode,
36
one must start the server once, before launching \texttt{why3 ide},
37 38 39 40
using
\begin{verbatim}
isabelle why3_jedit
\end{verbatim}
41
Then, inside a \texttt{why3 ide} session, any use of ``Edit'' will
42 43
transfer the file to the already opened instance of jEdit. When the
proof is completed, the user must send back the edited proof to
44
\texttt{why3 ide} by closing the opened buffer, typically by hitting
45
\texttt{Ctrl-w}.
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
\subsection{Using Isabelle 2018 server}

Starting from Isabelle version 2018, Why3 is able to exploit the
server features of Isabelle to speed up the processing of proofs in
batch mode, e.g. when replaying them from within Why3 IDE. Currently,
when replaying proofs using the \verb|isabelle why3| tool, an Isabelle
process including a rather heavyweight Java/Scala and PolyML runtime
environment has to be started, and a suitable heap image has to be
loaded for each proof obligation, which can take several seconds. To
avoid this overhead, an Isabelle server and a suitable session can be
started once, and then \verb|isabelle why3| can just connect to it and
request the server to process theories. In order to allow a tool such
as Why3 IDE to use the Isabelle server, it has to be started via the
wrapper tool \verb|isabelle use_server|. For example, to process the proofs
in examples/logic/genealogy using Why3 IDE and the Isabelle server, do
the following:
\begin{enumerate}
\item Start an Isabelle server using
\begin{verbatim}
   isabelle server &
\end{verbatim}
\item Start Why3 IDE using
\begin{verbatim}
   isabelle use_server why3 ide genealogy
\end{verbatim}
\end{enumerate}

 \subsection{Realizations}
MARCHE Claude's avatar
MARCHE Claude committed
75

Guillaume Melquiond's avatar
Guillaume Melquiond committed
76 77 78
Realizations must be designed in some \texttt{.thy} as follows.
The realization file corresponding to some \why file \texttt{f.why}
should have the following form.
MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82 83 84 85 86 87
\begin{verbatim}
theory Why3_f
imports Why3_Setup
begin

section {* realization of theory T *}

why3_open "f/T.xml"

Guillaume Melquiond's avatar
Guillaume Melquiond committed
88
why3_vc <some lemma>
MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94 95 96 97
<proof>

why3_vc <some other lemma> by proof

[...]

why3_end
\end{verbatim}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
98
See directory \texttt{lib/isabelle} for examples.
99 100 101 102 103 104 105


%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: