Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Intro.thy
changeset 440 a0b280dd4bc7
parent 435 524b72520c43
child 441 520127b708e6
equal deleted inserted replaced
439:b83c75d051b7 440:a0b280dd4bc7 
    23   \end{flushright}
 
    23   \end{flushright}
 
    24 
    24 
    25   \medskip
 
    25   \medskip
 
    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 researchers to play with Isabelle and implement
 
    29   the tutorial will encourage students and researchers to play with Isabelle
 
    30   new ideas. The source code of Isabelle can look intimidating, but beginners 
    30   and implement new ideas. The source code of Isabelle can look intimidating,
 
    31   can get by with knowledge of only a small number functions and a few basic
 
    31   but beginners can get by with knowledge of only a small number functions and
 
    32   coding conventions.
 
    32   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
 
    38   distribution.\footnote{\input{version}} If something does not work, then
 
    38   distribution.\footnote{\input{version}} If something does not work, then
 
    39   please let us know. It is impossible for us to know every environment,
 
    39   please let us know. It is impossible for us to know every environment,
 
    40   operating system or editor in which Isabelle is used. If you have comments,
 
    40   operating system or editor in which Isabelle is used. If you have comments,
 
    41   criticism or like to add to the tutorial, please feel free---you are most
 
    41   criticism or like to add to the tutorial, please feel free---you are most
 
    42   welcome! The tutorial is meant to be gentle and comprehensive. To achieve
 
    42   welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
 
    43   this we need your help and feedback.
 
    43   this we need your help and feedback.
 
    44 *}
 
    44 *}
 
    45 
    45 
    46 section {* Intended Audience and Prior Knowledge *}
 
    46 section {* Intended Audience and Prior Knowledge *}
 
    47 
    47 
    83   way things are actually implemented. More importantly, it is often
 
    83   way things are actually implemented. More importantly, it is often
 
    84   good to look at code that does similar things as you want to do and
 
    84   good to look at code that does similar things as you want to do and
 
    85   learn from it. This tutorial contains frequently pointers to the
 
    85   learn from it. This tutorial contains frequently pointers to the
 
    86   Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
 
    86   Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
 
    87   often your best friend while programming with Isabelle.\footnote{Or
 
    87   often your best friend while programming with Isabelle.\footnote{Or
 
    88   hypersearch if you program using jEdit under MacOSX.} To understand the sources,
 
    88   hypersearch if you work with jEdit under MacOSX.} To understand the sources,
 
    89   it is often also necessary to track the change history of a file or
 
    89   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/}} 
    90   files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 
    91   for Isabelle  provides convenient interfaces to query the history of
 
    91   for Isabelle  provides convenient interfaces to query the history of
 
    92   files and ``change sets''.
 
    92   files and ``change sets''.
 
    93   \end{description}
 
    93   \end{description}
 
   107   \end{graybox}
 
   107   \end{graybox}
 
   108   \end{isabelle}
 
   108   \end{isabelle}
 
   109   
   109   
   110   These boxes correspond to how code can be processed inside the interactive
 
   110   These boxes correspond to how code can be processed inside the interactive
 
   111   environment of Isabelle. It is therefore easy to experiment with the code
 
   111   environment of Isabelle. It is therefore easy to experiment with the code
 
   112   that is given in this tutorial. However, for better readability we will drop
 
   112   that is shown in this tutorial. However, for better readability we will drop
 
   113   the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
 
   113   the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
 
   114   write:
 
   114   write:
 
   115 
   115 
   116   @{ML [display,gray] "3 + 4"}
 
   116   @{ML [display,gray] "3 + 4"}
 
   117   
   117   
   133 
   133 
   134   \begin{readmore}
 
   134   \begin{readmore}
 
   135   Further information or pointers to files.
 
   135   Further information or pointers to files.
 
   136   \end{readmore}
 
   136   \end{readmore}
 
   137 
   137 
   138   The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
 
   138   Note that pointers to Isabelle files are hyperlinked to the tip of the Mercurial
 
   139   repository at \href{http://isabelle.in.tum.de/repos/isabelle/}
 
   139   repository at \href{http://isabelle.in.tum.de/repos/isabelle/}
 
   140   {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release
 
   140   {http://isabelle.in.tum.de/repos/isabelle/}, not the latest stable release
 
   141   of Isabelle.
 
   141   of Isabelle.
 
   142 
   142 
   143   A few exercises are scattered around the text. Their solutions are given 
   143   A few exercises are scattered around the text. Their solutions are given 
   144   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
 
   144   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
 
   145   to solve the exercises on your own, and then look at the solutions.
 
   145   to solve the exercises on your own, and then look at the solutions.
 
   146 *}
 
   146 *}
 
   147 
   147 
   148 section {* How To Understand Code in Isabelle *}
 
   148 section {* How To Understand Isabelle Code *}
 
   149 
   149 
   150 text {*
 
   150 text {*
 
   151   One of the more difficult aspects of programming is to understand somebody
 
   151   One of the more difficult aspects of any kind of programming is to understand code
 
   152   else's code. This is aggravated in Isabelle by the fact that many parts of
 
   152   written by somebody else. This is aggravated in Isabelle by the fact that many parts of
 
   153   the code contain only few comments. There is one strategy that might be
 
   153   the code contain none or only few comments. There is one strategy that might be
 
   154   helpful to navigate your way: ML is an interactive programming environment,
 
   154   helpful to navigate your way: ML is an interactive programming environment,
 
   155   which means you can evaluate code on the fly (for example inside an
 
   155   which means you can evaluate code on the fly (for example inside an
 
   156   \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy
 
   156   \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy
 
   157   self-contained chunks of existing code into a separate theory file and then
 
   157   (self-contained) chunks of existing code into a separate theory file and then
 
   158   study it alongside with examples. You can also install probes inside the
 
   158   study it alongside with examples. You can also install ``probes'' inside the
 
   159   copied code without having to recompile the whole Isabelle distributions. Such
 
   159   copied code without having to recompile the whole Isabelle distributions. Such
 
   160   probes might be messages or printouts of variables (see chapter
 
   160   probes might be messages or printouts of variables (see chapter
 
   161   \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
 
   161   \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
 
   162   probing the code with explicit print statements is the most efficient method
 
   162   probing the code with explicit print statements is the most effective method
 
   163   for understanding what some code is doing. However do not expect quick
 
   163   for understanding what some piece of code is doing. However do not expect quick
 
   164   results with this! Depending on the size of the code you are looking at, 
   164   results with this! Depending on the size of the code you are looking at, 
   165   you will spend the better part of a quiet afternoon with it. But there 
   165   you will spend the better part of a quiet afternoon with it. And there 
   166   seems to be no better way around it.
 
   166   seems to be no better way for understanding code in Isabelle.
 
   167 *}
 
   167 *}
 
   168 
   168 
   169 
   169 
   170 section {* Aaaaargh! My Code Does not Work Anymore *}
 
   170 section {* Aaaaargh! My Code Does not Work Anymore *}
 
   171 
   171 
   172 text {*
 
   172 text {*
 
   173   One unpleasant aspect of any code development inside a larger system is that
 
   173   One unpleasant aspect of any code development inside a larger system is that
 
   174   one has to aim at a ``moving target''. Isabelle is no exception. Every 
   174   one has to aim at a ``moving target''. Isabelle is no exception of this. Every 
   175   update lets potentially all hell break loose, because other developers have
 
   175   update lets potentially all hell break loose, because other developers have
 
   176   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   176   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   177   but taking the view that incompatible code changes are a fact of life 
   177   but taking the view that incompatible code changes are a fact of life 
   178   might be more gratifying. Isabelle is a research project. In most circumstances 
   178   might be more gratifying. Isabelle is a research project. In most circumstances 
   179   it is just impossible to make research backward compatible (imagine Darwin 
   179   it is just impossible to make research backward compatible (imagine Darwin
isabelle-cookbook