isabelle.tex 3.2 KB
 MARCHE Claude committed Feb 01, 2014 1 2 \section{Isabelle/HOL} \label{sec:isabelle}  MARCHE Claude committed Dec 08, 2013 3   MARCHE Claude committed Feb 01, 2014 4 5 \index{Isabelle proof assistant}  Guillaume Melquiond committed Jun 20, 2014 6 When using Isabelle from \why, files generated from \why theories and  MARCHE Claude committed Mar 13, 2014 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  MARCHE Claude committed Feb 01, 2016 10 using Edit'' action in \texttt{why3 ide}.  MARCHE Claude committed Mar 13, 2014 11   MARCHE Claude committed Feb 01, 2014 12 13 \subsection{Installation}  Stefan Berghofer committed Aug 20, 2018 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.  MARCHE Claude committed Feb 01, 2014 17   Guillaume Melquiond committed Jun 20, 2014 18 19 Isabelle must be installed before compiling \why. After compilation and installation of \why, you must manually add the path  MARCHE Claude committed Mar 13, 2014 20 21 22 \begin{verbatim} /isabelle \end{verbatim}  Guillaume Melquiond committed Jun 20, 2014 23 into either the user file  MARCHE Claude committed Mar 13, 2014 24 \begin{verbatim}  Stefan Berghofer committed Aug 20, 2018 25 .isabelle/Isabelle2018/etc/components  MARCHE Claude committed Mar 13, 2014 26 \end{verbatim}  Guillaume Melquiond committed Jun 20, 2014 27 or the system-wide file  MARCHE Claude committed Mar 13, 2014 28 29 30 \begin{verbatim} /etc/components \end{verbatim}  MARCHE Claude committed Feb 01, 2014 31 32  \subsection{Usage}  MARCHE Claude committed Feb 01, 2014 33   Guillaume Melquiond committed Jun 20, 2014 34 The most convenient way to call Isabelle for discharging a \why goal  MARCHE Claude committed Mar 13, 2014 35 is to start the Isabelle/jedit interface in server mode. In this mode,  MARCHE Claude committed Feb 01, 2016 36 one must start the server once, before launching \texttt{why3 ide},  MARCHE Claude committed Mar 13, 2014 37 38 39 40 using \begin{verbatim} isabelle why3_jedit \end{verbatim}  MARCHE Claude committed Feb 01, 2016 41 Then, inside a \texttt{why3 ide} session, any use of Edit'' will  MARCHE Claude committed Mar 13, 2014 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  MARCHE Claude committed Feb 01, 2016 44 \texttt{why3 ide} by closing the opened buffer, typically by hitting  MARCHE Claude committed Mar 13, 2014 45 \texttt{Ctrl-w}.  MARCHE Claude committed Feb 01, 2014 46   MARCHE Claude committed Aug 30, 2018 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 committed Dec 08, 2013 75   Guillaume Melquiond committed Jun 20, 2014 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 committed Dec 08, 2013 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 committed Jun 20, 2014 88 why3_vc  MARCHE Claude committed Dec 08, 2013 89 90 91 92 93 94 95 96 97  why3_vc by proof [...] why3_end \end{verbatim}  Guillaume Melquiond committed Jun 20, 2014 98 See directory \texttt{lib/isabelle} for examples.  MARCHE Claude committed Feb 01, 2014 99 100 101 102 103 104 105  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: