[isabelle-dev] Isatest

Makarius makarius at sketis.net
Wed Mar 28 21:11:44 CEST 2012


On Wed, 28 Mar 2012, Florian Haftmann wrote:

> Once there has been the idea that everyone having commit access to the 
> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a 
> isatest subscriber.
>
> Maybe it would be helpful to establish this as a rule (at least of 
> thumb).  Isatest mails can still be sorted out by local email filters.
>
> What do you think?

I could imagine some reforms in the meaning of the Unix group "isabelle" 
and how it is managed, although I have a tendency to leave the status-quo 
untouched.

For every administrative facility that is added, one also needs to take 
maintenance into account.  Last weekend I had to spend more time to figure 
out why isatest did not send any mails at all, than who needs to be added 
to the list.

Who is the main responsible for isatest anyway?  According to the received 
customs it would be Gerwin, since he started the service many years ago. 
(His shell scripts still mention SunOS.)


Yet a different angle on the situation is to de-centralize a few things 
that are not essential for the main Isabelle repository.  I have already 
started to do a few small-scale things independently via bitbucket, which 
I would have done via the Isabelle repos some years ago.

This does not mean that I have any concrete proposals in the pocket, let's 
say about using a really really good issue tracker service on some open 
source hosting platform -- if it exists at all.


 	Makarius



More information about the isabelle-dev mailing list