Re: [Hol-info] How do I reinitialize HOL in the command window?

[Ramana Kumar]

To add to that, I don't think github provides great hosting of plain old
HTML files the way sourceforge does. I could be wrong.

On Tue, Jul 31, 2012 at 12:45 AM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:

> On 31/07/12 06:25, Ian Zimmerman wrote:
>
> > Michael> I'm glad you got the emacs mode to work.  There’s some
> > Michael> (recently updated) documentation for it at
>
> > Michael>http://hol.sourceforge.net/hol-mode.html
>
> > Why on sourceforge?  Shouldn't _everything_ migrate to github?
>
> I can't see why, offhand.  The main argument against is that it's nice to
> have a
> consistent URL (I think we've had this one for 10 years or so) and e-mail
> addresses.  The sources for the web-pages are stored on github (see
> https://github.com/mn200/hol-webpages), but I think our user-facing world
> can
> remain on sourceforge.  We also use sourceforge for this (and other)
> mailing
> lists and (mirrored) file-hosting.
>
> There's a pretty simple message: users see us at sourceforge, developers
> interact with github facilities.  I get to be the guy that straddles both
> worlds, developing on github of course, but also occasionally pushing
> releases
> and web-page updates to sourceforge.
>
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

On 31/07/12 06:25, Ian Zimmerman wrote:

> Michael> I'm glad you got the emacs mode to work.  There’s some
> Michael> (recently updated) documentation for it at

> Michael>http://hol.sourceforge.net/hol-mode.html

> Why on sourceforge?  Shouldn't _everything_ migrate to github?

I can't see why, offhand.  The main argument against is that it's nice to have 
a 
consistent URL (I think we've had this one for 10 years or so) and e-mail 
addresses.  The sources for the web-pages are stored on github (see 
https://github.com/mn200/hol-webpages), but I think our user-facing world can 
remain on sourceforge.  We also use sourceforge for this (and other) mailing 
lists and (mirrored) file-hosting.

There's a pretty simple message: users see us at sourceforge, developers 
interact with github facilities.  I get to be the guy that straddles both 
worlds, developing on github of course, but also occasionally pushing releases 
and web-page updates to sourceforge.

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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Ian Zimmerman]

Michael> I'm glad you got the emacs mode to work.  There’s some
Michael> (recently updated) documentation for it at

Michael>http://hol.sourceforge.net/hol-mode.html

Why on sourceforge?  Shouldn't _everything_ migrate to github?

-- 
Ian Zimmerman
gpg public key: 1024D/C6FF61AD
fingerprint: 66DC D68F 5C1B 4D71 2EE5  BD03 8A00 786C C6FF 61AD
http://www.gravatar.com/avatar/c66875cda51109f76c6312f4d4743d1e.png
Rule 420: All persons more than eight miles high to leave the court.

--
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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Gottfried Barrow]

On 7/6/2012 7:05 AM, Makarius wrote:
http://www.tug.org/texlive/ seems to support Cygwin directly by its 
own installer, without going through the Cygwin package management.  
So it might be worth trying that.


That might be worth a try for me. MiKTeX is set to ask me if I want it 
to go retrieve an uninstalled package, so I guess TeXLive might do the 
same thing.


MiKTeX has a portable install that you could put under your contrib, and 
then call into it with Java. It's download size is 157 megabytes.


http://miktex.org/portable/about

But switching from teTex is trivial compared to porting Poly/ML to a 
native Windows.


You need a big grant from the Templeton Foundation:

http://www.templeton.org/what-we-fund/core-funding-areas

http://www.templeton.org/what-we-fund/core-funding-areas/science-and-the-big-questions/mathematical-and-physical-sciences

Spin it that 
the new action in abstract, non-applied, proof-emphasized mathematics is 
going to be driven by automated proof checking. That's the way it's 
gonna be. Research into numerical analysis and numerical solutions 
consumes much of the resources in mathematics departments; it's part of 
the PC revolution.


It's a waste of everyone's time for proofs to be "pencil and paper" from 
beginning to end. Tell the Templeton Foundation that, and you might get 
a grant, or maybe not.


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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Makarius]

On Wed, 27 Jun 2012, Gottfried Barrow wrote:

> An issue being migrating off of teTeX, if you want to completely get off 
> of Cygwin.
>
> In Cygwin setup, it shows tetex-extra at version 3.0.0-3.
>
> At http://www.tug.org/tetex/, it says:
>
>   I (Thomas Esser) have decided not to make new releases of teTeX any
>   more (May 2006). The information below might get out of date as time
>   goes by.
>
> But I have batch files and scripts to compile highlighted sections of
> LaTeX with MiKTeX. To compile LaTeX through "isabelle latex" would
> complicate things, and then Cygwin teTeX being old complicates things,
> so I stick with what's been working for me, but someday I might want
> antiquotations.

http://www.tug.org/texlive/ seems to support Cygwin directly by its own 
installer, without going through the Cygwin package management.  So it 
might be worth trying that.


> I haven't done anything to change the setup for ~~/contrib/cygwin-1.7.9.

Cygwin from 2012 poses some challenges to threads and sockets in Poly/ML, 
rendering it quite unstable for big applications.  This is why I have 
downgraded to cygwin-1.7.9 from spring 2011.

I hope to pick up this loose thread again together with David Matthews. 
It is one of the motivations to take Poly/ML on MinGW into account more 
seriously.  Another would be native x86_64 support that is still unavaible 
for Cygwin after so many years.

This might be also relevant to HOL maintainers, who want to move towards 
more serious support of Poly/ML and Windows.


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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Gottfried Barrow]

On 6/24/2012 2:49 PM, Makarius wrote:
> 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...

An issue being migrating off of teTeX, if you want to completely get off 
of Cygwin.

In Cygwin setup, it shows tetex-extra at version 3.0.0-3.

At http://www.tug.org/tetex/, it says:

   I (Thomas Esser) have decided not to make new releases of teTeX any
   more (May 2006). The information below might get out of date as time
   goes by.

At http://ctan.org/pkg/tetex, it says:

   In 2006, Thomas Esser announced he would no longer be able to
   support, or to produce new versions of, teTeX. With the appearance of
   TeX live 2007 (whose Unix-system TeX support originally derived from
   teTeX), no-one should be using teTeX at all, in new applications.

I haven't installed tetex-extra to be able to build the PDF documents 
for Isabelle2012. For Isabelle2011, it worked. I think I manually placed 
a few packages in the teTeX texmf folder.

But I have batch files and scripts to compile highlighted sections of 
LaTeX with MiKTeX. To compile LaTeX through "isabelle latex" would 
complicate things, and then Cygwin teTeX being old complicates things, 
so I stick with what's been working for me, but someday I might want 
antiquotations.

But calling commands like "isabelle jedit" or "isabelle browser" is 
pretty transparent. I wouldn't want to do without Cygwin without a 
replacement for it.

I still have a different copy of Cygwin installed for Isabelle2011-1. I 
haven't done anything to change the setup for ~~/contrib/cygwin-1.7.9. 
All I did was find out what the new path to bash is.

--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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Makarius]

On Mon, 25 Jun 2012, Michael Norrish wrote:

> On 25/06/12 05:49, Makarius wrote:
>
>> The bare-bones Cygwin with perl
>> and python weights merely 100 MB, the JRE/JDK 200 MB, and avarage Isabelle 
>> logic
>> image 150 MB.

> 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.

Past versions of Cygwin had this principle that there can be only one 
cygwin.dll installed on the system.  So putting one version of it here 
would prevent to install another version there.  Moreover, the installer 
would change various registry entries globally that then affect other 
Cygwins.

With more recent Cygwin 1.7.x is has become possible to make a 
"pre-canned" Cygwin installation that does not affect anything else.  In 
Isabelle2012 I have packaged it like that for the first time, hopefully 
with some success.  I have also changed some defaults to make HOME the 
actual Windows home, not the one of that particular copy of Cygwin.

This is becoming more and more alien to the Unix guy, but Windows users 
feel more at home with it.


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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Makarius]

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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

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 
shared 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.

> 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. 
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.

Best,
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

On 6/11/2012 7:05 PM, Michael Norrish wrote:
> I've made Konrad's suggested change in the repository so that users of
> future releases won't hit the same problem.
>
> You can see the revised file at
>
> https://raw.github.com/mn200/HOL/e8110e6d9c03e54685f30f216357f77ef380b8f2/examples/euclid.sml
>
> Best,
> Michael

I have been known to be involved in making great contributions towards 
resolving trivial problems.

My response here is just an excuse to speak informally concerning your 
Emacs hol-mode.el interface, which I've now experimented with.

Dude, the Emacs interface to HOL4 is awesome.

I can't believe I was going to try and do this stuff without it. With 
split screens and the ability to send highlighted text to the prover 
with various commands, that's great.

I customize Emacs enough to make it friendlier. Tabs at the top relieve 
the stress on my stack when lots of files are open:
 https://github.com/dholm/tabbar

Other easy customizing:
 http://xahlee.org/emacs/emacs_make_modern.html

--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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

On 12/06/12 11:45, gottfried.bar...@gmx.com wrote:

> Emacs will be good, once it becomes less mysterious. Vi is also pretty
> mysterious. Both require a deeper stack than I prefer to use.

I hope the menus in Emacs are some help.  The HOL menu captures most of the 
emacs mode's functionality.

> 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

--
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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

On 6/11/2012 7:36 PM, Michael Norrish wrote:

 > I'm glad you got the emacs mode to work. There’s some (recently
 > updated) documentation for it at
 >
 > http://hol.sourceforge.net/hol-mode.html

I used "(load "/tools/hol-mode")" from that file, and the 3 
Emacs commands at this FAQ page link to enable the Unicode:
 http://hol.sourceforge.net/faq.html#Parsing

 > Incidentally, there is also a vim-mode if you prefer that editor, but
 > I suspect it won't work on Windows.
 >
 > Best,
 > Michael

Emacs will be good, once it becomes less mysterious. Vi is also pretty 
mysterious. Both require a deeper stack than I prefer to use.

But I may try out HOL4 under Linux someday for the Poly/ML speed.

Thanks,
--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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

> I got hol-mode.el running under Emacs, with the unicode working right.
>   http://ftp.gnu.org/gnu/emacs/windows/

> The unicode didn't work with a Windows command console, so I had to
> disable it.

> Emacs is a lot better, including the HOL character highlighting, and the
> X-windows part of XEmacs has never helped me figure out the many
> mysteries of how to use Emacs.

I'm glad you got the emacs mode to work.  There’s some (recently updated) 
documentation for it at

   http://hol.sourceforge.net/hol-mode.html

Let me know if you run into any issues using the hol-mode.

Incidentally, there is also a vim-mode if you prefer that editor, but I suspect 
it won't work on Windows.

Best,
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Michael Norrish]

I've made Konrad's suggested change in the repository so that users of future 
releases won't hit the same problem.

You can see the revised file at

https://raw.github.com/mn200/HOL/e8110e6d9c03e54685f30f216357f77ef380b8f2/examples/euclid.sml

Best,
Michael

On 12/06/12 05:29, Konrad Slind wrote:
>>> Send (or post) a minimal failing version and the maintainers can help
>>> you.
>>
>> I thought it was me causing problems by loading my own scripts after
>> "HOL/examples/euclid.sml", but it wasn't.
>
> The failure comes from making the "divides" constant an infix after its
> definition. All is fine the first time around, but the second time the file
> is used, divides is encountered in prefix position, but is expected to be
> in infix position. Here's the change, which sets the fixity status of
> the identifier,
> then makes the definition.
>
>  set_fixity "divides" (Infix(NONASSOC, 450));
>
>  val divides_def =
>   Define
>`a divides b = ?x. b = a * x`;
>
>
> Konrad.
>
> --
> 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


--
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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

On 6/11/2012 2:29 PM, Konrad Slind wrote:
> Here's the change, which sets the fixity status of
> the identifier, then makes the definition.
>
>  set_fixity "divides" (Infix(NONASSOC, 450));
>
>  val divides_def =
>   Define
>`a divides b = ?x. b = a * x`;
> Konrad.

That's good to know.

I got hol-mode.el running under Emacs, with the unicode working right.
 http://ftp.gnu.org/gnu/emacs/windows/

The unicode didn't work with a Windows command console, so I had to 
disable it.

Emacs is a lot better, including the HOL character highlighting, and the 
X-windows part of XEmacs has never helped me figure out the many 
mysteries of how to use Emacs.

Thanks again,
-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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Konrad Slind]

>> Send (or post) a minimal failing version and the maintainers can help
>> you.
>
> I thought it was me causing problems by loading my own scripts after
> "HOL/examples/euclid.sml", but it wasn't.

The failure comes from making the "divides" constant an infix after its
definition. All is fine the first time around, but the second time the file
is used, divides is encountered in prefix position, but is expected to be
in infix position. Here's the change, which sets the fixity status of
the identifier,
then makes the definition.

set_fixity "divides" (Infix(NONASSOC, 450));

val divides_def =
 Define
  `a divides b = ?x. b = a * x`;


Konrad.

--
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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[gottfried . barrow]

On 6/11/2012 12:26 PM, Konrad Slind wrote:
 > On Mon, Jun 11, 2012 at 1:12 AM,  wrote:

 > On windows I usually run HOL4 under emacs. But of course that's
 > just personal preference.

I tried to load hol-mode.el in xemacs running under Cygwin, but I 
couldn't get it to work.

 >> I close the HOL4 window, and then start HOL4 again, but it doesn't
 >> start up instantly.
 >
 > I haven't encountered this problem (on XP).

I just meant that it takes 15 seconds for HOL4 to load after the console 
window comes up. If it takes me 5 seconds to edit a script, and I run it 
40 times, 15 seconds is a long time to wait.

I've figured out my solution: start 3 HOL4 sessions at a time so I don't 
have to wait after a session goes bad.

 > Send (or post) a minimal failing version and the maintainers can help
 > you.

I thought it was me causing problems by loading my own scripts after 
"HOL/examples/euclid.sml", but it wasn't.

I don't really care about these errors, since it's not my fault, but 
here's the input and output (I typed it by hand, so there might be some 
errors):

 - use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
 ...goes through the proof
 > val EUCLID_AGAIN = |- !n. ?p. n < p /\ prime p : thm
 [closing file "C:\Users\jv\AppData\Local\Temp\mosml68.hol"]
 > val it = () : unit
 - use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
 [opening file "C:\Users\jv\AppData\Local\Temp\mosml69.hol"]
 on line 23, characters 3-13:
 No rule for [divides, TM]

 Exception raised at Absyn.Absyn:
 on line 23, characters 3-31:
 No rule for [divides, TM]
 ! Uncaught exception:
 ! HOL_ERR
 [closing file "C:\users\jv\AppData\Local\Temp\mosml69.hol"]
 -

Konrad, thanks for the information.

--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

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Konrad Slind]

On Mon, Jun 11, 2012 at 1:12 AM,   wrote:
> I'm using HOL4 in the Windows console. I load a file using the "use"
> command, like this:
>
> use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
>

On windows I usually run HOL4 under emacs. But of course that's
just personal preference.

> I then edit some ML scripts in an editor and load them into HOL4 using
> the "use" command. My scripts get errors, so when I try to load
> "euclid.sml" again as shown above, I get errors in HOL4 which I didn't
> get before.

Most operations in HOL4 have been designed to be idempotent, i.e.,
if you call them once without error, you should be able to call them
again without error (and get the same result!). However, HOL4 does
have some internal state which can get muddled by re-invocations.
In some cases, this has to do with the HOL4 grammar. SML itself can
fail on re-invocation, typically with "infix" declarations.

Send (or post) a minimal failing version and the maintainers can help
you.

> I close the HOL4 window, and then start HOL4 again, but it doesn't start
> up instantly.

I haven't encountered this problem (on XP).

> Is there a command I can use to reinitialize HOL4 without closing it and
> restarting it?

I don't think so.


Cheers,
Konrad.

--
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