[isabelle-dev] Repository Trouble

[Lawrence Paulson]

I don't remember where I got it from. Probably from the last time this sort of thing happened (only the current episodes have been much worse).

I can't think of a stronger case for using an alias than the present situation, where using the wrong machine can corrupt the repository. Where several man-days were lost solving the problem. Sure, everybody can update their hgrc file to refer to lxbroy10, but what happens when it needs to be shut down for some reason?

Larry

On 3 Jan 2013, at 14:33, Makarius <makarius at sketis.net> wrote:

> On Wed, 2 Jan 2013, Lawrence Paulson wrote:
> 
>> I have been using
>> 
>> 	hgbroy.informatik.tu-muenchen.de
>> 
>> under the assumption that the name hgbroy could be expected to refer to a suitable machine.
> 
> From where did you get that?  hgbroy seems to be an alias of the old cvsbroy, and probably refers to some other hg server experiment at TUM. I've occasionally called it "home-made" -- it was very crude at the start, but I did not check it again.  Checking the host briefly, hgbroy does not look like one of these patched SuSE machines, but why use it instead of lxbroy10 -- the standard Isabelle server right now?
> 
> It is very difficult to keep an overview of the many things happening internally at TUM, but we don't have to do that by sticking to proper Isabelle/Admin documentation.  When Alex had pointed out lxbroy10 as the canonical solution, I had updated the all-important README_REPOSITORY here http://isabelle.in.tum.de/repos/isabelle/rev/9df2f825422b
> 
> 
> 	Makarius
>