[isabelle-dev] Small repository accident
makarius at sketis.net
Fri Feb 24 21:50:18 CET 2012
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
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.
More information about the isabelle-dev