[isabelle-dev] Reasons mira crashes

Makarius makarius at sketis.net
Thu Nov 29 11:28:39 CET 2012

On Thu, 29 Nov 2012, Lars Noschinski wrote:

>> So we still carry a lot of CVS baggage stemming from 1993, not just in
>> the low-level technological sense.
>> Nothing new, all known already. I usually ignore it to avoid the trouble
>> of thinking about more fundamental changes.
> We could make up a rule "always go through host X" (X being one of the 
> macbroys/lxbroys) and hope it is the simultaneous access from multiple 
> hosts and not the fact that it is laying on a NFS which makes it 
> unreliable.

I've been thinking of this occasionally, but it does not work either, 
because the "gateway" systems that are reachable for ssh from outside are 
fluctuating a lot.  It used to be just atbroy100 as canonical example some 
years ago, then one had to shuffle macbroy20..29 to get some machine that 
happens to be available, now one occasioanlly needs to take the lxlabbroy 
into account.  I edit my .hg/hgrc a lot these days.

On Wed, 28 Nov 2012, Makarius wrote:

> On Wed, 28 Nov 2012, Gerwin Klein wrote:
>> This may be entirely unrelated, but I've just had to re-clone the afp hg
>> repository in my home directory at TUM because it made mercurial crash on
>> pull, and failed integrity checking.
>> The only other time I've ever had to do that in the past few years of using
>> mercurial was because of file corruption due to a broken hard disk (two
>> cases). If this happens frequently to us, something may be very wrong with
>> storage on the macbroy/lxbroy machines.
> The reliability of NFS at TUM has indeed degraded a bit, maybe already more
> than 5 years ago, but it is hard to pin down.

I now remember the difference from distant past.  Until approx. 5-6 years 
ago, the NFS server (first sunbroy60, then sunbroy1, then sunbroy2) was 
accessible by ssh. Thus everybody was using that for his ssh login in the 
cvs configuration, because it made things much faster with the local 
harddisk access on the remote host.  So neither the NFS problem nor the 
client program confusion did exist.

Then the NFS server was made more "secure", so users could no longer 
login.  I also remember now that it was the point where cvs became 
unbearably slow, and thus accelerated our move to state-of-the-art version 
control, where central transactions only happen occasionally (pull, push) 
and not for every single commit (which is hard to imagine now).

So if there is an easy solution to more robust access of some file system 
served at TUM, I am for it.  Anything beyond that should be a move away 
from home-made servers to some professional hosting platform like 
Bitbucket (not Sourceforge, not Google code).  Note that we have already 
several home-made services running that are only half-maintained, and we 
cannot afford this for the main collection point of Isabelle changesets.


More information about the isabelle-dev mailing list