26 If your next project requires you to program on the ML-level of Isabelle, |
26 If your next project requires you to program on the ML-level of Isabelle, |
27 then this tutorial is for you. It will guide you through the first steps of |
27 then this tutorial is for you. It will guide you through the first steps of |
28 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
28 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
29 the tutorial will encourage students and researchers to play with Isabelle |
29 the tutorial will encourage students and researchers to play with Isabelle |
30 and implement new ideas. The source code of Isabelle can look intimidating, |
30 and implement new ideas. The source code of Isabelle can look intimidating, |
31 but beginners can get by with knowledge of only a small number of functions |
31 but beginners can get by with knowledge of only a handful of concepts, |
32 and a few basic coding conventions. |
32 a small number of functions and a few basic coding conventions. |
33 |
33 |
34 |
34 |
35 The best way to get to know the ML-level of Isabelle is by experimenting |
35 The best way to get to know the ML-level of Isabelle is by experimenting |
36 with the many code examples included in the tutorial. The code is as far as |
36 with the many code examples included in the tutorial. The code is as far as |
37 possible checked against the Isabelle |
37 possible checked against the Isabelle |
49 This tutorial targets readers who already know how to use Isabelle for |
49 This tutorial targets readers who already know how to use Isabelle for |
50 writing theories and proofs. We also assume that readers are familiar with |
50 writing theories and proofs. We also assume that readers are familiar with |
51 the functional programming language ML, the language in which most of |
51 the functional programming language ML, the language in which most of |
52 Isabelle is implemented. If you are unfamiliar with either of these two |
52 Isabelle is implemented. If you are unfamiliar with either of these two |
53 subjects, then you should first work through the Isabelle/HOL tutorial |
53 subjects, then you should first work through the Isabelle/HOL tutorial |
54 \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. |
54 \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently, |
|
55 Isabelle has adopted a sizable amount of Scala code for a slick GUI |
|
56 based on jEdit. This part of the code is beyond the interest of this |
|
57 tutorial, since it mostly does not concern the regular Isabelle |
|
58 developer. |
55 *} |
59 *} |
56 |
60 |
57 section {* Existing Documentation *} |
61 section {* Existing Documentation *} |
58 |
62 |
59 text {* |
63 text {* |
78 Then of course there are: |
82 Then of course there are: |
79 |
83 |
80 \begin{description} |
84 \begin{description} |
81 \item[The Isabelle sources.] They are the ultimate reference for how |
85 \item[The Isabelle sources.] They are the ultimate reference for how |
82 things really work. Therefore you should not hesitate to look at the |
86 things really work. Therefore you should not hesitate to look at the |
83 way things are actually implemented. More importantly, it is often |
87 way things are actually implemented. While much of the Isabelle |
84 good to look at code that does similar things as you want to do and |
88 code is uncommented, some parts have very helpful comments---particularly |
85 learn from it. This tutorial contains frequently pointers to the |
89 the code about theorems and terms. Despite the lack of comments in most |
|
90 parts, it is often good to look at code that does similar things as you |
|
91 want to do and learn from it. |
|
92 This tutorial contains frequently pointers to the |
86 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
93 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
87 often your best friend while programming with Isabelle.\footnote{Or |
94 often your best friend while programming with Isabelle.\footnote{Or |
88 hypersearch if you work with jEdit.} To understand the sources, |
95 hypersearch if you work with jEdit.} To understand the sources, |
89 it is often also necessary to track the change history of a file or |
96 it is often also necessary to track the change history of a file or |
90 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
97 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
146 *} |
153 *} |
147 |
154 |
148 section {* How To Understand Isabelle Code *} |
155 section {* How To Understand Isabelle Code *} |
149 |
156 |
150 text {* |
157 text {* |
151 One of the more difficult aspects of any kind of programming is to understand code |
158 One of the more difficult aspects of any kind of programming is to |
152 written by somebody else. This is aggravated in Isabelle by the fact that many parts of |
159 understand code written by somebody else. This is aggravated in Isabelle by |
153 the code contain none or only few comments. There is one strategy that might be |
160 the fact that many parts of the code contain none or only few |
154 helpful to navigate your way: ML is an interactive programming environment, |
161 comments. There is one strategy that might be helpful to navigate your way: |
155 which means you can evaluate code on the fly (for example inside an |
162 ML is an interactive programming environment, which means you can evaluate |
156 \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy |
163 code on the fly (for example inside an \isacommand{ML}~@{text |
157 (self-contained) chunks of existing code into a separate theory file and then |
164 "\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained) |
158 study it alongside with examples. You can also install ``probes'' inside the |
165 chunks of existing code into a separate theory file and then study it |
159 copied code without having to recompile the whole Isabelle distribution. Such |
166 alongside with examples. You can also install ``probes'' inside the copied |
|
167 code without having to recompile the whole Isabelle distribution. Such |
160 probes might be messages or printouts of variables (see chapter |
168 probes might be messages or printouts of variables (see chapter |
161 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
169 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
162 probing the code with explicit print statements is the most effective method |
170 probing the code with explicit print statements is the most effective method |
163 for understanding what some piece of code is doing. However do not expect quick |
171 for understanding what some piece of code is doing. However do not expect |
164 results with this! Depending on the size of the code you are looking at, |
172 quick results with this! It is painful. Depending on the size of the code |
165 you will spend the better part of a quiet afternoon with it. And there |
173 you are looking at, you will spend the better part of a quiet afternoon with |
166 seems to be no better way for understanding code in Isabelle. |
174 it. And there seems to be no better way for understanding code in Isabelle. |
167 *} |
175 *} |
168 |
176 |
169 |
177 |
170 section {* Aaaaargh! My Code Does not Work Anymore *} |
178 section {* Aaaaargh! My Code Does not Work Anymore *} |
171 |
179 |