ProgTutorial/Intro.thy
changeset 486 45cfd2ece7bd
parent 485 f3536f0b47a9
child 502 615780a701b6
equal deleted inserted replaced
485:f3536f0b47a9 486:45cfd2ece7bd
   219 text {*
   219 text {*
   220   As already pointed out in the previous section, Isabelle is a joint effort 
   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
   221   of many developers. Therefore, disruptions that break the work of others
   222   are generally frowned upon. ``Accidents'' however do happen and everybody knows
   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 
   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
   224   sophisticated \emph{testboard}, which will perform checks of your changes against the
   225   Isabelle repository and against the AFP. The advantage of the testboard is
   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
   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 
   227   tests on, for example, your own laptop. You can see the results of the testboard 
   228   at 
   228   at 
   229 
   229 
   230   \begin{isabelle}
   230   \begin{center}
   231   ??
   231   \url{http://isabelle.in.tum.de/testboard/Isabelle/}
   232   \end{isabelle}
   232   \end{center}
   233 
   233 
   234   which is organised like a Mercurial repository. A green point next to a change
   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
   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 
   236   have to allow some time). You can summit any changes to the testboard using the 
   237 
   237   command
   238   \begin{isabelle}
   238 
   239   \begin{tabular}{@ {}l}
   239   @{text [display] "$ hg push -f ssh://...@macbroy21.informatik.tu-muenchen.de\\
   240   @{text "[path]"}\\
   240    //home/isabelle-repository/repos/testboard"}
   241   @{text "testboard = "}
   241 
   242   \end{tabular}
   242   where the dots need to be replaced by your login name.  Note that for
   243   \end{isabelle}
   243   pushing changes to the testboard you need to add the option @{text "-f"},
   244 
   244   which however should \emph{never} be used with the main Isabelle
   245   to your Mercurial settings file. Then you can test any changes using the command
   245   repository. While the testboard is a great system for supporting Isabelle
   246 
   246   developers, its disadvantage is that it needs login permissions for the
   247   @{text [display] "$ hg push -f testboard"}
   247   computers in Munich. So in order to use it, you might have to ask other
   248 
   248   developers to obtain one.
   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 *}
   249 *}
   255 
   250 
   256 
   251 
   257 section {* Some Naming Conventions in the Isabelle Sources *}
   252 section {* Some Naming Conventions in the Isabelle Sources *}
   258 
   253