[isabelle-dev] push request (Sublist.thy)

[Makarius]

On Thu, 13 Dec 2012, Dmitriy Traytel wrote:

> Stripping did not work (even on lxbroy10 with some older Mercurial). 
> However, Johannes managed to apparently fix everything by doing a fresh 
> clone, copying some files (such as hgrc) and adjusting permissions (cf. 
> https://isabelle.in.tum.de/community/Reconstructing_the_Isabelle_repository).

This is a serious problem, not just in a technical sense.

Why is there again this diverging clone of important administrative 
information?  So the community wiki is not about Isabelle community at 
all, but to make administration harder by putting unreliable information 
snippets on a virtual whiteboard.  It actually causes dis-unity not 
com-unity.


When I did the re-cloning last time, I documented it explicitly in 
http://isabelle.in.tum.de/repos/isabelle/rev/71136069089d see also 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02978.html

Our main tools for Isabelle development are the repistory and the 
isabelel-dev mailing list.  I am not even a user of the Isabelle community 
wiki, and will not maintain all this divergence of clones.


We probably also need to rethink the hosting problem of the conventional 
push-area for the central clone of the Isabelle reposity.  A single 
dropout every 2 years would be acceptable, but not several times in 1 
year.  Maybe there is a chance to discuss it with Franz Huber next week, 
and a solution without home-made servers.  Otherwise we need an external 
hosting service, which is relatively easy.  It will be reletively hard to 
sort out the administrative structure, though, since we are still stuck in 
the "everybody is root" paradigm stemming from CVS 1.0.


 	Makarius