diff -r c0cae24b9d46 -r 5dffcab68680 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Sat Oct 03 13:01:39 2009 +0200 +++ b/ProgTutorial/Intro.thy Sat Oct 03 19:10:23 2009 +0200 @@ -36,7 +36,7 @@ writing theories and proofs. We also assume that readers are familiar with the functional programming language ML, the language in which most of Isabelle is implemented. If you are unfamiliar with either of these two - subjects, you should first work through the Isabelle/HOL tutorial + subjects, then you should first work through the Isabelle/HOL tutorial \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. *} @@ -68,7 +68,8 @@ things really work. Therefore you should not hesitate to look at the way things are actually implemented. More importantly, it is often good to look at code that does similar things as you want to do and - learn from it. The UNIX command \mbox{@{text "grep -R"}} is + learn from it. This tutorial contains frequently pointers to the + Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is often your best friend while programming with Isabelle, or hypersearch if you program using jEdit under MacOSX. To understand the sources, it is often also necessary to track the change history of a file or @@ -82,7 +83,7 @@ text {* All ML-code in this tutorial is typeset in shaded boxes, like the following - ML-expression: + simple ML-expression: \begin{isabelle} \begin{graybox} @@ -133,7 +134,7 @@ text {* One unpleasant aspect of any code development inside a larger system is that - one has to aim at a ``moving target''. The Isabelle system is no exception. Every + one has to aim at a ``moving target''. Isabelle is no exception. Every update lets potentially all hell break loose, because other developers have changed code you are relying on. Cursing is somewhat helpful in such situations, but taking the view that incompatible code changes are a fact of life @@ -141,31 +142,31 @@ it is just impossible to make research backward compatible (imagine Darwin attempting to make the Theory of Evolution backward compatible). - However, there are a few steps you can take to mitigate unwanted interferences - with code changes from other developers. First, you can base your code on the latest - stable release of Isabelle (it is aimed to have one such release at least - once every year). This - might cut you off from the latest feature - implemented in Isabelle, but at least you do not have to track side-steps - or dead-ends in the Isabelle development. Of course this means also you have - to synchronise your code at the next stable release. Another possibility - is to get your code into the Isabelle distribution. For this you have - to convince other developers that your code or project is of general interest. - If you managed to do this, then the problem of the moving target goes - away, because when checking in new code, developers are strongly urged to - test it against Isabelle's code base. If your project is part of that code base, - then maintenance is done by others. Unfortunately, this might not - be a helpful advice for all types of projects. A lower threshold for inclusion has the - Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} - This archive has been created mainly for formalisations that are - interesting but not necessarily of general interest. If you have ML-code as - part of a formalisation, then this might be the right place for you. There - is no problem with updating your code after submission. At the moment - developers are not as diligent with checking their code against the AFP than - with checking agains the distribution, but generally problems will be caught - and the developer, who caused them, is expected to fix them. So also - in this case code maintenance is done for you. - + However, there are a few steps you can take to mitigate unwanted + interferences with code changes from other developers. First, you can base + your code on the latest stable release of Isabelle (it is aimed to have one + such release at least once every year). This might cut you off from the + latest feature implemented in Isabelle, but at least you do not have to + track side-steps or dead-ends in the Isabelle development. Of course this + means also you have to synchronise your code at the next stable release. If + you do not synchronise, be warned that code seems to ``rot'' very + quickly. Another possibility is to get your code into the Isabelle + distribution. For this you have to convince other developers that your code + or project is of general interest. If you managed to do this, then the + problem of the moving target goes away, because when checking in new code, + developers are strongly urged to test it against Isabelle's code base. If + your project is part of that code base, then maintenance is done by + others. Unfortunately, this might not be a helpful advice for all types of + projects. A lower threshold for inclusion has the Archive of Formalised + Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive + has been created mainly for formalisations that are interesting but not + necessarily of general interest. If you have ML-code as part of a + formalisation, then this might be the right place for you. There is no + problem with updating your code after submission. At the moment developers + are not as diligent with checking their code against the AFP than with + checking agains the distribution, but generally problems will be caught and + the developer, who caused them, is expected to fix them. So also in this + case code maintenance is done for you. *} section {* Some Naming Conventions in the Isabelle Sources *} @@ -208,7 +209,7 @@ \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} - and helped with recipe \ref{rec:timing}. Parts of the section \ref{sec:storing} + and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} are by him. \item {\bf Jeremy Dawson} wrote the first version of the chapter