--- a/ProgTutorial/FirstSteps.thy Wed Jun 24 15:58:59 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Tue Jul 14 01:42:35 2009 +0200
@@ -57,7 +57,7 @@
code, rather they indicate what the response is when the code is evaluated.
There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
including ML-code. The first evaluates the given code, but any effect on the
- ambient theory is suppressed. The second needs to be used if ML-code is defined
+ `ambient' theory is suppressed. The second needs to be used if ML-code is defined
inside a proof. For example
\begin{quote}
@@ -69,8 +69,8 @@
\end{isabelle}
\end{quote}
- However, both commands will not play any role in this tutorial (we, for example,
- always assume the ML-code is defined outside proofs).
+ However, both commands will only play minor roles in this tutorial (we will always
+ arrange that the ML-code is defined outside of proofs).
Once a portion of code is relatively stable, you usually want to export it
to a separate ML-file. Such files can then be included somewhere inside a
@@ -102,7 +102,11 @@
\end{tabular}
\end{quote}
- Note that no parentheses are given this time.
+ Note that no parentheses are given this time. Note also that the
+ `used' file should not contain any
+ \isacommand{use} itself. Otherwise Isabelle is unable to record all
+ file dependencies, which is a nuisance if you have to track down
+ errors.
*}
section {* Debugging and Printing\label{sec:printing} *}
@@ -230,12 +234,12 @@
In order to improve the readability of theorems we convert
these schematic variables into free variables using the
- function @{ML [index] import_thms in Variable}.
+ function @{ML [index] import in Variable}.
*}
ML{*fun no_vars ctxt thm =
let
- val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+ val ((_, [thm']), _) = Variable.import true [thm] ctxt
in
thm'
end
@@ -630,6 +634,26 @@
kinds of logical elements from the ML-level.
*}
+text {* FIXME: an example of a user defined antiquotation *}
+
+ML{*ML_Antiquote.inline "term_pat"
+ (Args.context -- Scan.lift Args.name_source >>
+ (fn (ctxt, s) =>
+ let
+ val t = ProofContext.read_term_pattern ctxt s
+ in
+ ML_Syntax.atomic (ML_Syntax.print_term t)
+ end))*}
+
+ML{*@{term_pat "?x + ?y"}*}
+
+text {*
+
+ \begin{readmore}
+ @{ML_file "Pure/ML/ml_antiquote.ML"}
+ \end{readmore}
+*}
+
section {* Terms and Types *}
text {*
@@ -1700,9 +1724,7 @@
@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
\begin{readmore}
- For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
- the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
- data.
+ For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
\end{readmore}
(FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
--- a/ProgTutorial/Intro.thy Wed Jun 24 15:58:59 2009 +0200
+++ b/ProgTutorial/Intro.thy Tue Jul 14 01:42:35 2009 +0200
@@ -62,9 +62,14 @@
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
often your best friend while programming with Isabelle, or
- hypersearch if you program using jEdit under MacOSX.
+ 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
+ files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
+ for Isabelle provides convenient interfaces to query the history of
+ files and ``change sets''.
\end{description}
+
*}
section {* Typographic Conventions *}
@@ -119,6 +124,45 @@
to solve the exercises on your own, and then look at the solutions.
*}
+section {* Aaaaargh! My Code Does not Work Anymore *}
+
+text {*
+ One unpleasant aspect of any code development inside a larger system is that
+ one has to aim for a ``moving target''. The Isabelle system 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
+ might be more gratifying. Isabelle is a research project. In most circumstances
+ 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 code, developers are strongly urged to
+ test against Isabelle's code base. If your project is part of that code base,
+ then code 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 *}
text {*
@@ -141,12 +185,6 @@
\end{itemize}
*}
-section {* Aaaaargh! My Code Does not Work Anymore (TBD) *}
-
-text {*
-
-*}
-
section {* Acknowledgements *}
text {*
Binary file progtutorial.pdf has changed