206 code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained) |
206 code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained) |
207 chunks of existing code into a separate theory file and then study it |
207 chunks of existing code into a separate theory file and then study it |
208 alongside with examples. You can also install ``probes'' inside the copied |
208 alongside with examples. You can also install ``probes'' inside the copied |
209 code without having to recompile the whole Isabelle distribution. Such |
209 code without having to recompile the whole Isabelle distribution. Such |
210 probes might be messages or printouts of variables (see chapter |
210 probes might be messages or printouts of variables (see chapter |
211 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
211 \ref{chp:firststeps}). Moreover, PolyML contains a debugger that is also supported from Isabelle/jEdit |
212 probing the code with explicit print statements is the most effective method |
212 with breakpoints and stack inspection. |
|
213 Still it seems that |
|
214 probing the code with explicit print statements is an effective method |
213 for understanding what some piece of code is doing. However do not expect |
215 for understanding what some piece of code is doing. However do not expect |
214 quick results with this! It is painful. Depending on the size of the code |
216 quick results with this! It is painful. Depending on the size of the code |
215 you are looking at, you will spend the better part of a quiet afternoon with |
217 you are looking at, you will spend the better part of a quiet afternoon with |
216 it. And there seems to be no better way for understanding code in Isabelle. |
218 it. And there seems to be no better way for understanding code in Isabelle. |
|
219 Summarizing: |
|
220 \begin{itemize} |
|
221 \item Get familiar with the concepts and the applications by studying the Isabelle/Isar |
|
222 reference manual and the rich set of theories and libraries in the standard distribution and the AFP. |
|
223 \item Get familiar with the implementation and the best practices (like coding style, |
|
224 canonical argument ordering, \<open>\<dots>\<close>) by reading the Isabelle/Isar implementation manual and by |
|
225 browsing, reading and digesting both the code implementing a function as well and the |
|
226 applications of that function. |
|
227 \item Interactively experiment with the code. |
|
228 \end{itemize} |
|
229 |
217 \<close> |
230 \<close> |
218 |
231 |
219 |
232 |
220 section \<open>Aaaaargh! My Code Does not Work Anymore\<close> |
233 section \<open>Aaaaargh! My Code Does not Work Anymore\<close> |
221 |
234 |