[isabelle-dev] Isatest

Tobias Nipkow nipkow at in.tum.de
Thu Mar 29 07:31:11 CEST 2012


Am 28/03/2012 23:30, schrieb Gerwin Klein:
> On 29/03/2012, at 6:11 AM, Makarius wrote:
> 
>> 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. 
> 
> Yes, that is the main problem I see with this (otherwise I'm all for it). If there is an email list that automatically contains everyone with push-access, emails could easily be sent there. I wouldn't want to have to maintain that email list, tough.

Florian suggested "a rule (of thumb)", not automation. Hence I am still in
favour. It just means that whoever grants write access should try and remember
to add that person to the email list.

Tobias

> 
>> 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.)
> 
> They do ;-)
> 
> I still feel mildly responsible for isatest, but would be more than happy to pass this on to somebody with more time and more close in time(zone) and and space to where it actually runs.
> 
> Cheers,
> Gerwin
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



More information about the isabelle-dev mailing list