On 6/12/2012 1:03 AM, Michael Norrish wrote: > On 12/06/12 11:45, gottfried.bar...@gmx.com wrote:
> I hope the menus in Emacs are some help. The HOL menu captures most of > the emacs mode's functionality. They definitely look good to me. The way I was going to do things, using an external editor and "use", there wasn't going to be a lot of "interactive proving" in it, or it was going to be a hassle to do. >> But I may try out HOL4 under Linux someday for the Poly/ML speed. > > One option I've considered is the development of a standard virtualbox > image of (Linux + Poly + HOL) that Windows users could use from within > Windows. > > Michael I have VirtualBox installed (https://www.virtualbox.org/), and I have an installation of Linux that I could fire up, but I don't like becoming dependent on Linux applications. 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. With the GNU Emacs I installed today, I can drag files into it. There's no integration problem with all the other Windows editors and document processing programs that I use. 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. As far as the X-windows part of Cygwin, there's something messed up about that. The Emacs I'm using looks much better than the Cygwin XEmacs. With Cygwin, you have to start the X-windows console, and then you start XEmacs, and it's not the latest version, so a lot of Emacs scripts don't work good. If you have a Windows installation of something that installs fairly easily, then it lowers the requirements. But if there's multiple installations of software, then lots of people won't want to go through the hassles of dealing with another operating system. 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