[isabelle-dev] Cygwin isatest

[Makarius]

This is an intermediate report of the somewhat delayed efforts for routine 
support of Cygwin in isatest.  It is mainly relevant to people on the 
internal isatest mailing list.

Cygwin can be understood as a fairly standard GNU/Linux distribution, that 
happens to have a non-standard kernel produced by a company in Redmond. 
Together with the Cygwin sshd, it is possible to use it in some kind of 
multi-user server mode that provides the expected look-and-feel of command 
line interaction, without funny windows getting in between.

Isabelle support for Cygwin became official with Isabelle2008, and has 
further improved in the Isabelle2009 and Isabelle2009-1 releases.  The 
user base for that platform has been growing continously, and there are 
some indications that it has already surpassed Mac OS.  In particular, 
most mathematicians seem to be locked into the Windows platform.

This means Cygwin platform testing needs to be taken more seriously.  In 
the current isatest setup there are still some rough edges, but I am glad 
to see that it did almost get through today.

The machine being used here is atbroy102, which is a Windows 7 box with 
very rigid security settings behind a firewall.  Access via ssh works by 
sending me a public key, and I will manually set up an account.  (This is 
really ssh only, without any provisions to mount remote file systems, and 
without remote desktop access.)

Concerning the state of affairs of Isabelle platforms in general, there 
are some explanations in Admin/PLATFORMS.  This does not affect anything 
run in pure ML, of course.


 	Makarius