On Thu, 14 Jun 2012, Michael Norrish wrote:
> On 12/06/12 16:59, [email protected] wrote:
>
>> There's Cygwin. The Isabelle group somehow makes that work with
>> Poly/ML. A huge part of why Cygwin is a good solution, though, is the
>> jEdit interface.
>
> Yes. We could put some effort into making HOL work with Poly/ML and
> Cygwin.
There are several things involved here, and somehow mixed up.
The classic arrangement before Isabelle2012 was to use Cygwin + its X11 +
its XEmacs (or GNU Emacs for X11) with Proof General. With Isabelle/jEdit
in Isabelle2012 it is now native Windows Java + jEdit (plain jar stuff),
and Cygwin only for Poly/ML and add-on tools (ATPs for Sledgehammer). So
the fragile and awkward Cygwin/X11 could be discontinued.
> I'm a bit reluctant to force people to adopt large chunks of software
> (like Cygwin) that aren't strictly necessary, but Poly/ML is so much
> faster than Moscow ML that Windows users really are missing out.
The meaning of "large" is changing over time. The bare-bones Cygwin with
perl and python weights merely 100 MB, the JRE/JDK 200 MB, and avarage
Isabelle logic image 150 MB. (You are not using images in HOL4, right?).
Generally, my experience with Windows support (2008..2012) is this:
(1) Initially I tried the Virtual Machine appliance scheme (with VMware
player, before Virtualbox became publicly available). This
compelling idea was discontinued for the following reasons:
- The basic Linux installation (Ubuntu) for the image already
requires 1-2 GB, so this is going to be a really large chunk.
- Configuring the virtual Linux after starting up is not so easy.
Even basic things like timezone or keymaps need to be
reconsidered. (Maybe there are now Linux distributions to make
that work out smoothly.) Network and printer connections not
counted yet.
- Windows users don't feel at home on the virtual Linux desktop.
Otherwise they would use Linux to begin with, and run Windows as
virtual machine within that.
(2) Later I tried to package up everything nicely within Cygwin, asking
users to install that first, and issued some obvious Unix-style
commands on the Cygwin terminal to install the system. This often
caused surprising problems for Windows users, such as unpacking tars
with Windoes 7zip and thus loosing important Posix file information.
(3) Now in Isabelle2012 everything is wrapped up as something that looks
like a genuine Windows application, using 7zip with a simple add-on
self-extracting installer. There are still a few intrusions of Cygwin
into the editor user space, e.g. certain error messages with
Posix file names that are apt to confuse windows users.
Note that since the start of the year 2012, Cygwin poses some challanges
to Poly/ML with sockets + multithreading in combination. For this reason,
I shall reconsider this basis and try to use Poly/ML compiled with MinGW
natively on Windows. This will certainly pose new issues, but I hope for
David Matthews (and maybe some Poly/ML power users) to help out. For
Isabelle, the ML process will probably be encapsulated within the
Scala/JVM wrapper, without terminal interaction. For HOL4, the latter
would still be needed, but one could try with Msys on MinGW, which appears
to include a library to pretend that there is a Unix-style terminal
available.
So in conclusion, extra platform support for Windows is not for free.
Cumulatively, the amount of annoyance accumulated in supporting it is
about the same as that for Mac OS X, with its very strange interpretation
of "Unix". But that is a different story.
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
