[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

[Makarius]

On Thu, 5 Jul 2012, Gerwin Klein wrote:

> lxbroy2 still has hickups.

Things are slowly getting better.  See also Isabelle/cd0a411b7fc1 where 
some pseudo-component settings are adjusted to the de-factor situation 
both on SuSE and Gentoo at TUM.


> Every 10 years or so stuff like this should be thrown out and rewritten.

There should be a continuous rewrite, but it has never happened.  Only 
addition of more and more features without deleting old things.


> Also, I really need to give this responsibility to somebody else. I'm 
> becoming too busy to really take care of isatest and it's beginning to 
> show in its stability.
>
> Consider this a call for volunteers!

There is still this ongoing process to replace isatest by mira.  What is 
still missing of the latter is at least this:

   * Clear entry point for the relevant information.  This should be
     Admin/mira/ within the official repository, not some world writable
     wiki with poor version control
     https://isabelle.in.tum.de/community/Main_Page

     Half of the community wiki pages are outdated.  Is the mira one
     current?

     There should be also some reliable information where to find the
     official mira repository, say within Admin/mira/README.

   * Some statistics like
     http://isabelle.in.tum.de/devel/stats/at-poly.html

     It does not have to be imitated literally.  The important thing is to
     see both performance trends and isolated spikes, on a linear thread of
     incoming changesets.

   * More proactive indication of failure of the official repository
     version, analogous to the isatest email notification.

   * Some way to test the forked isabelle-release repository in the
     critical phase of 2-3 weeks before a release, when the regular
     repository is already continuing in post-release mode.

     For Isabelle2012 we've had an annoying accident here that lead to the
     situation that Linux users cannot use nohup, because I've
     misinterpreted the mix of problems with the testing infrastructure
     that we've had, and thus overlooked the genuine SIGHUP issue.


 	Makarius