ProgTutorial/Intro.thy
changeset 580 883ce9c7b13b
parent 578 69c78980c8a4
equal deleted inserted replaced
579:4dc20f6921d0 580:883ce9c7b13b
   286   that the testing is performed by rather powerful machines saving you lengthy
   286   that the testing is performed by rather powerful machines saving you lengthy
   287   tests on, for example, your own laptop. You can see the results of the testboard 
   287   tests on, for example, your own laptop. You can see the results of the testboard 
   288   at 
   288   at 
   289 
   289 
   290   \begin{center}
   290   \begin{center}
   291   \url{http://isabelle.in.tum.de/testboard/Isabelle/}
   291   \url{https://ci.isabelle.systems/status}
   292   \end{center}
   292   \end{center}
   293 
   293 
   294   which is organised like a Mercurial repository. A green point next to a change
   294   You can summit any changes to the Isabelle testboard using the 
   295   indicates that the change passes the corresponding tests (for this of course you
       
   296   have to allow some time). You can summit any changes to the testboard using the 
       
   297   command
   295   command
   298 
   296 
   299   @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\
   297   @{text [display] "$ hg push -f ssh://...@isabelle-server.in.tum.de//home/isabelle-repository\\  
   300    //home/isabelle-repository/repos/testboard"}
   298   /repos/testboard"}
   301 
   299 
   302   where the dots need to be replaced by your login name.  Note that for
   300   and to the AFP testboard
   303   pushing changes to the testboard you need to add the option \<open>-f\<close>,
   301 
   304   which should \emph{never} be used with the main Isabelle
   302   @{text [display] "$ hg push -f ssh://hg@bitbucket.org/isa-afp/afp-testboard"}
   305   repository. While the testboard is a great system for supporting Isabelle
   303 
   306   developers, its disadvantage is that it needs login permissions for the
   304   where the dots in the first command need to be replaced by your
   307   computers in Munich. So in order to use it, you might have to ask other
   305   login name.  Note that for pushing changes to the testboard you need
   308   developers to obtain one.
   306   to add the option \<open>-f\<close>, which should \emph{never} be
   309 \<close>
   307   used with the main Isabelle repository. While the testboard is a
       
   308   great system for supporting Isabelle developers, its disadvantage is
       
   309   that it needs login permissions for the computers in Munich. So in
       
   310   order to use it, you might have to ask other developers to obtain
       
   311   one.  \<close>
   310 
   312 
   311 
   313 
   312 section \<open>Some Naming Conventions in the Isabelle Sources\<close>
   314 section \<open>Some Naming Conventions in the Isabelle Sources\<close>
   313 
   315 
   314 text \<open>
   316 text \<open>