On 6/13/2012 11:09 PM, Michael Norrish wrote: > On 12/06/12 16:59, gottfried.bar...@gmx.com wrote: > >> One major issue for me is the problem of editing the same file on >> Windows and Linux at the same time. I can't drag and drop files into >> Linux applications, and files don't always update correctly between >> the Windows and Linux applications. > > Hmm. Yes, that's not ideal. I understood that it was possible to > have files hared between the host and client machine in a transparent > way. If that's not really the case, then the virtual machine > approach is clearly sub-par.
I think a virtual machine running Linux could be a good solution in spite of the quirks. What doesn't solve the problem for Windows users is when a Windows user has to log into a Linux desktop. They're gonna be lost and just stare at the screen. If you can put a Windows application window on top of Linux, then that's the kind of thing people would know how to use. If people get a window under Windows, they know how to deal with that. If there were minor window refresh quirks, and a Windows editor and Linux editor didn't work together perfectly when editing the same file, and you couldn't drag and drop files into the application, that kind of thing might be manageable. >> 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. The thing with Cygwin is that the setup only offers XEmacs v21.4.22. That could be due to the limitations of the X11 X-windows server. I don't know why they're not improving the Cygwin windows interface, but you'd do a lot of work, and then you'd be tied into a clunky looking, old X-windows interface. > 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. A lot of people would rather download a 300Mbyte application that works by magic than a 30Mbyte application that requires a lot of tweaking to get going. The good news is that, up to this point, I've found the speed of the Moscow ML distribution to be acceptable. It takes 15 seconds to load HOL. It takes 30 seconds to run euclid.sml with this: val () = quietdec := false; open arithmeticTheory; val () = quietdec := false; It takes 8 seconds to run it with this: val () = quietdec := true; open arithmeticTheory; val () = quietdec := false; I only need to see screen displays for my working code. If the above performance will get me through the tutorial and a little beyond, then it's gonna work. If you know I'm in for a rude awakening, then maybe you shouldn't destroy the bliss of my ignorance at this time. The new Windows users are going to be newbies, and there will a large attrition rate amongst them. The Moscow ML distribution needs to be fast enough to get them up to speed. It doesn't have to be the complete, Windows solution. Once they're vested in HOL4, then they will have incentive to transition into Linux, if they have to. If you can work magic, and put an interface on Poly/ML running on Linux, and it runs 10 times faster, then of course we users would want that. But my motivation is low for working in Linux. Suppose I make some educational material on HOL4. Would a part of it be teaching people how to install Linux on top of Windows, and then install Poly/ML in Linux, and then HOL4 in Linux? No. That wouldn't work. I'm not complaining. We're all limited by the OS cards we've been dealt. I have HOL4 running in Emacs. It's working so far, not that I've worked it much. Regards, GB ------------------------------------------------------------------------------ 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