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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
