[isabelle-dev] Cygwin isatest
makarius at sketis.net
Wed Apr 21 12:22:11 CEST 2010
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.
More information about the isabelle-dev