# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320518668 0
# Node ID f3536f0b47a9618eef8180d3021e42ea8e85b1ba
# Parent  490fe9483c0dadf97a51d9fb6a2f33969d708780
added section about testboard

diff -r 490fe9483c0d -r f3536f0b47a9 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Fri Nov 04 09:29:50 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Sat Nov 05 18:44:28 2011 +0000
@@ -73,22 +73,26 @@
 section {* Setups (TBD) *}
 
 text {*
-  In the previous section we used \isacommand{setup}, for example, in
-  order to make a theorem attribute known to Isabelle. What happens
-  behind the scenes is that \isacommand{setup} expects a function of
-  type @{ML_type "theory -> theory"}: the input theory is the current
-  theory and the output the theory where the theory attribute has been
+  In the previous section we used \isacommand{setup} in order, for example, 
+  to make a theorem attribute known to Isabelle or register a theorem under
+  a name. What happens behind the scenes is that \isacommand{setup} expects a 
+  function of type @{ML_type "theory -> theory"}: the input theory is the current
+  theory and the output the theory where the theory attribute or theorem has been
   stored.
 
   This is a fundamental principle in Isabelle. A similar situation arises
   with declaring constants. The function that declares a 
   constant on the ML-level is @{ML_ind  declare_const in Sign}. 
-  However, if you simply write\footnote{Recall that ML-code  needs to be 
+  However, note that if you simply write\footnote{Recall that ML-code  needs to be 
   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
 *}  
 
-ML{*Sign.declare_const @{context} 
-  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) @{theory} *}
+ML{*let
+  val thy = @{theory}
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
+in 
+  Sign.declare_const @{context} bar_const thy  
+end*}
 
 text {*
   with the intention of declaring the constant @{text "BAR"} with type @{typ nat} 
@@ -96,22 +100,25 @@
   query the constant on the Isabelle level using the command \isacommand{term}
 
   \begin{isabelle}
-  \isacommand{term}~@{text [quotes] "BAR"}\\
+  \isacommand{term}~@{text BAR}\\
   @{text "> \"BAR\" :: \"'a\""}
   \end{isabelle}
 
-  you can see that you do not obtain a constant of type @{typ nat}, but a free 
+  you can see that you do \emph{not} obtain a constant of type @{typ nat}, but a free 
   variable (printed in blue) of polymorphic type. The problem is that the 
   ML-expression above did not ``register'' the declaration with the current theory. 
   This is what the command \isacommand{setup} is for. The constant is properly 
   declared with
 *}
 
-setup %gray {* Sign.declare_const @{context} 
-  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) #> snd *}
+setup %gray {* let
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
+in 
+  Sign.declare_const @{context} bar_const #> snd 
+end *}
 
 text {* 
-  Now 
+  where the declaration is actually applied to the theory and
   
   \begin{isabelle}
   \isacommand{term}~@{text [quotes] "BAR"}\\
@@ -120,6 +127,12 @@
 
   returns a (black) constant with the type @{typ nat}, as expected.
 
+  In a sense, \isacommand{setup} can be seen as a transaction that takes the
+  current theory, applies an operation, and produces a new current theory. This
+  means that we have to be careful to apply operations always to the current
+  theory, not to a \emph{stale} one. The code below produces
+
+
   A similar command is \isacommand{local\_setup}, which expects a function
   of type @{ML_type "local_theory -> local_theory"}. Later on we will also
   use the commands \isacommand{method\_setup} for installing methods in the
diff -r 490fe9483c0d -r f3536f0b47a9 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Fri Nov 04 09:29:50 2011 +0000
+++ b/ProgTutorial/Intro.thy	Sat Nov 05 18:44:28 2011 +0000
@@ -214,6 +214,46 @@
   case code maintenance is done for you.
 *}
 
+section {* Serious Isabelle ML-Programming *}
+
+text {*
+  As already pointed out in the previous section, Isabelle is a joint effort 
+  of many developers. Therefore, disruptions that break the work of others
+  are generally frowned upon. ``Accidents'' however do happen and everybody knows
+  this. Still to keep them to a minimum, you can submit your changes first to a rather 
+  sophisticated \emph{testboard}, which will perform checks of your changes agains the
+  Isabelle repository and against the AFP. The advantage of the testboard is
+  that the testing is performed by rather powerful machines, saving you lengthy
+  tests on, for example, your laptop. You can see the results of the testboard 
+  at 
+
+  \begin{isabelle}
+  ??
+  \end{isabelle}
+
+  which is organised like a Mercurial repository. A green point next to a change
+  indicates that the change passes the corresponding tests (for this of course you
+  have to allow some time). To facilitate the use of the testboard you should add 
+
+  \begin{isabelle}
+  \begin{tabular}{@ {}l}
+  @{text "[path]"}\\
+  @{text "testboard = "}
+  \end{tabular}
+  \end{isabelle}
+
+  to your Mercurial settings file. Then you can test any changes using the command
+
+  @{text [display] "$ hg push -f testboard"}
+
+  Note that for pushing changes to the testboard you need to add the option @{text "-f"},
+  which however should \emph{never} be used with the main Isabelle repository. While
+  the testboard is a great system for supporting Isabelle developers, its 
+  disadvantage is that it needs login permissions for the computers in Munich. So in order 
+  to use it, you might have to ask other developers.
+*}
+
+
 section {* Some Naming Conventions in the Isabelle Sources *}
 
 text {*
diff -r 490fe9483c0d -r f3536f0b47a9 progtutorial.pdf
Binary file progtutorial.pdf has changed