[isabelle-dev] repos integrity

Makarius makarius at sketis.net
Thu Jun 18 19:55:17 CEST 2009


Dear Isabelle contributors,

just a few very basic things that are so obvious that they seem to have 
been forgotten.

   * The main Isabelle repository http://isabelle.in.tum.de/repos/isabelle
     always needs to be in a state where

       isabelle makeall all

     finishes succesfully!  Experienced Isabelle developers should already
     know that the quantum dynamics of the system make it practically
     impossible to predict the result of that test run -- it really needs
     to be done experimentally.

     With the separation of commit vs push in Mercurial, there is really
     no excuse if this is omitted.  If repository integrity is broken,
     others need to spend extra time on that (recently it has happened all
     the time).

   * The same essentially holds for AFP, but since it is not on Mercurial
     yet, it is hard to synchronize pushes here vs. commits there.  So AFP
     tests can come a bit later (hours or days, but not weeks).

   * Any "user-relevant changes" should be documented in NEWS (say within
     1-2 weeks after a push, afterwards it is usually forgotton).

   * Any relevant contribution should get an entry in CONTRIBUTORS.


 	Makarius



More information about the isabelle-dev mailing list