[isabelle-dev] Reasons mira crashes

Lars Noschinski noschinl at in.tum.de
Thu Nov 29 11:45:40 CET 2012


On 29.11.2012 11:28, Makarius wrote:
> On Thu, 29 Nov 2012, Lars Noschinski wrote:
>> 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.

I now wanted to suggest isabelle.in.tum.de as an obvious choice for a 
gateway host, but it is not reachable via SSH from the outside =)

> 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.

I will ask the MTAs about that. Since some time they also provide 
hosting of mercurial repositories.

   -- Lars



More information about the isabelle-dev mailing list