# HG changeset patch # User Christian Urban # Date 1247528555 -7200 # Node ID 195c4444dff76f269773337a35786eb204ca1a6c # Parent e0049c84278530b193e943ab2d337846e4f33154 added section about code maintenance and added an example for antiquotations diff -r e0049c842785 -r 195c4444dff7 ProgTutorial/FirstSteps.thy --- 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"}?) diff -r e0049c842785 -r 195c4444dff7 ProgTutorial/Intro.thy --- 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 {* diff -r e0049c842785 -r 195c4444dff7 progtutorial.pdf Binary file progtutorial.pdf has changed