On Thu, 14 Jun 2012, Michael Norrish wrote: > On 12/06/12 16:59, gottfried.bar...@gmx.com 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info