60 things really work. Therefore you should not hesitate to look at the |
60 things really work. Therefore you should not hesitate to look at the |
61 way things are actually implemented. More importantly, it is often |
61 way things are actually implemented. More importantly, it is often |
62 good to look at code that does similar things as you want to do and |
62 good to look at code that does similar things as you want to do and |
63 learn from it. The UNIX command \mbox{@{text "grep -R"}} is |
63 learn from it. The UNIX command \mbox{@{text "grep -R"}} is |
64 often your best friend while programming with Isabelle, or |
64 often your best friend while programming with Isabelle, or |
65 hypersearch if you program using jEdit under MacOSX. |
65 hypersearch if you program using jEdit under MacOSX. To understand the sources, |
|
66 it is often also necessary to track the change history of a file or |
|
67 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
|
68 for Isabelle provides convenient interfaces to query the history of |
|
69 files and ``change sets''. |
66 \end{description} |
70 \end{description} |
|
71 |
67 |
72 |
68 *} |
73 *} |
69 |
74 |
70 section {* Typographic Conventions *} |
75 section {* Typographic Conventions *} |
71 |
76 |
115 {http://isabelle.in.tum.de/repos/isabelle/}. |
120 {http://isabelle.in.tum.de/repos/isabelle/}. |
116 |
121 |
117 A few exercises are scattered around the text. Their solutions are given |
122 A few exercises are scattered around the text. Their solutions are given |
118 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
123 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
119 to solve the exercises on your own, and then look at the solutions. |
124 to solve the exercises on your own, and then look at the solutions. |
|
125 *} |
|
126 |
|
127 section {* Aaaaargh! My Code Does not Work Anymore *} |
|
128 |
|
129 text {* |
|
130 One unpleasant aspect of any code development inside a larger system is that |
|
131 one has to aim for a ``moving target''. The Isabelle system is no exception. Every |
|
132 update lets potentially all hell break loose, because other developers have |
|
133 changed code you are relying on. Cursing is somewhat helpful in such situations, |
|
134 but taking the view that incompatible code changes are a fact of life |
|
135 might be more gratifying. Isabelle is a research project. In most circumstances |
|
136 it is just impossible to make research backward compatible (imagine Darwin |
|
137 attempting to make the Theory of Evolution backward compatible). |
|
138 |
|
139 However, there are a few steps you can take to mitigate unwanted interferences |
|
140 with code changes from other developers. First, you can base your code on the latest |
|
141 stable release of Isabelle (it is aimed to have one such release at least |
|
142 once every year). This |
|
143 might cut you off from the latest feature |
|
144 implemented in Isabelle, but at least you do not have to track side-steps |
|
145 or dead-ends in the Isabelle development. Of course this means also you have |
|
146 to synchronise your code at the next stable release. Another possibility |
|
147 is to get your code into the Isabelle distribution. For this you have |
|
148 to convince other developers that your code or project is of general interest. |
|
149 If you managed to do this, then the problem of the moving target goes |
|
150 away, because when checking in code, developers are strongly urged to |
|
151 test against Isabelle's code base. If your project is part of that code base, |
|
152 then code maintenance is done by others. Unfortunately, this might not |
|
153 be a helpful advice for all types of projects. A lower threshold for inclusion has the |
|
154 Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} |
|
155 This archive has been created mainly for formalisations that are |
|
156 interesting but not necessarily of general interest. If you have ML-code as |
|
157 part of a formalisation, then this might be the right place for you. There |
|
158 is no problem with updating your code after submission. At the moment |
|
159 developers are not as diligent with checking their code against the AFP than |
|
160 with checking agains the distribution, but generally problems will be caught |
|
161 and the developer, who caused them, is expected to fix them. So also |
|
162 in this case code maintenance is done for you. |
|
163 |
120 *} |
164 *} |
121 |
165 |
122 section {* Some Naming Conventions in the Isabelle Sources *} |
166 section {* Some Naming Conventions in the Isabelle Sources *} |
123 |
167 |
124 text {* |
168 text {* |
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
183 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
140 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
184 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
141 \end{itemize} |
185 \end{itemize} |
142 *} |
186 *} |
143 |
187 |
144 section {* Aaaaargh! My Code Does not Work Anymore (TBD) *} |
|
145 |
|
146 text {* |
|
147 |
|
148 *} |
|
149 |
|
150 section {* Acknowledgements *} |
188 section {* Acknowledgements *} |
151 |
189 |
152 text {* |
190 text {* |
153 Financial support for this tutorial was provided by the German |
191 Financial support for this tutorial was provided by the German |
154 Research Council (DFG) under grant number URB 165/5-1. The following |
192 Research Council (DFG) under grant number URB 165/5-1. The following |