On 6/13/2012 11:09 PM, Michael Norrish wrote:
> On 12/06/12 16:59, [email protected] 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
