On 25/06/12 05:49, Makarius wrote: > 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 pleased to say that we have no dependencies on X11, so would be able to do without Cygwin/X11 pain. >> 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?). Poly/ML HOL users do use heaps. The standard HOL heap is 55MB; a subsequent heap containing a bunch of theories to do with the lambda calculus that I used in my computability work is 69MB. Disk space is cheap of course, so being too worried about space is perhaps not such a big deal. More worrying perhaps is the thought that users may not appreciate having new systems thrown onto their computers if doing so affects things other than their theorem-proving. My limited experience with Cygwin (independent of any theorem-proving, and a while ago now) is that it could make its presence felt, even in areas where it was not wanted. This nice separation of concerns is one reason why the virtual machine approach is superficially appealing... > 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. Thanks for sharing this experience; it does make the whole thing sound rather unappealing after all. > 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. MacOS provides no problems for HOL4 at all. Poly/ML HOL builds "out of the box". For Moscow ML, the dynamic linking of C code is slightly trickier to get working because of minor differences in the C environment. This dynamic linking of C code is only used by people wanting to use linked BDDs (which I suspect is just about nobody). Michael ------------------------------------------------------------------------------ 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
