[isabelle-dev] Small repository accident

[Makarius]

On Fri, 24 Feb 2012, Alexander Krauss wrote:

> The practical issues it adresses: It gives you convenient and fast 
> feedback about whether Isabelle_makeall on your changeset(s) succeeds. 
> In particular, it is useful if you do not have a fast machine for 
> yourself.

It also makes the results persistent -- at least that was one of the 
initial motivations.  Did that work out in retrospective?

Concerning "a fast machine for yourself", I do it the old-fashioned way 
via rsync and then test remotely in batch mode before committing.


Another old-fashioned mode of operation is to make a remote shell session 
for the front-end, so one could test such things interactively.  Proof 
General used to have some rsh feature, before ssh even existed, but it 
seems now out-of-use or discontinued.

When doing the local socket connection for Scala <-> ML for Windows/Cygwin 
(where a plain named pipe is unreliable), I realized again that one could 
somehow make non-local sockets part of the game by default.  This is 
particularly relevant for Swing applications, because X11 display 
forwarding does not really work here.


 	Makarius