217 section {* Serious Isabelle ML-Programming *}

   218 

   219 text {*

   220   As already pointed out in the previous section, Isabelle is a joint effort 

   221   of many developers. Therefore, disruptions that break the work of others

   222   are generally frowned upon. ``Accidents'' however do happen and everybody knows

   223   this. Still to keep them to a minimum, you can submit your changes first to a rather 

   224   sophisticated \emph{testboard}, which will perform checks of your changes agains the

   225   Isabelle repository and against the AFP. The advantage of the testboard is

   226   that the testing is performed by rather powerful machines, saving you lengthy

   227   tests on, for example, your laptop. You can see the results of the testboard 

   228   at 

   229 

   230   \begin{isabelle}

   231   ??

   232   \end{isabelle}

   233 

   234   which is organised like a Mercurial repository. A green point next to a change

   235   indicates that the change passes the corresponding tests (for this of course you

   236   have to allow some time). To facilitate the use of the testboard you should add 

   237 

   238   \begin{isabelle}

   239   \begin{tabular}{@ {}l}

   240   @{text "[path]"}\\

   241   @{text "testboard = "}

   242   \end{tabular}

   243   \end{isabelle}

   244 

   245   to your Mercurial settings file. Then you can test any changes using the command

   246 

   247   @{text [display] "$ hg push -f testboard"}

   248 

   249   Note that for pushing changes to the testboard you need to add the option @{text "-f"},

   250   which however should \emph{never} be used with the main Isabelle repository. While

   251   the testboard is a great system for supporting Isabelle developers, its 

   252   disadvantage is that it needs login permissions for the computers in Munich. So in order 

   253   to use it, you might have to ask other developers.

   254 *}

   255 

   256