Re: [Hol-developers] [Hol-checkins] SF.net SVN: hol:[6896] HOL/examples/machine-code

[Michael N. <Mic...@ni...>]

Anthony Fox wrote:

>  From reading this thread, I'm not entirely clear as to why the
> standard kernel isn't building in Poly/ML.  Is it the use of MosmlML
> specific features/libraries?  Or is it that Poly/ML is failing for
> some other reason?

It's a bug in Poly/ML: it raises an internal compiler error.

> It would be nice to carry out an official poll of users... I have
> moved to using Poly/ML (on Linux and Mac).  I understand that there
> are some users of Mosml on Windows, so that would be an interesting
> stat.

I don't know if there are any users of HOL on Windows.  Sourceforge
reports lots of downloads of the relevant installer, but I'm not sure
what that proves.

> Porting to Ocaml or F# would be a big (not necessarily popular)
> move.  If that were done then you might as well re-engineer HOL at
> the same time, with more emphasis on performance and with a more
> modern interface (giving our shift keys a well earned rest).
> However, I suspect that HOL light may be a better source for such an
> activity.  Besides, I very much doubt that there are the resources
> or the will for such an activity -- a lot has been invested the
> existing HOL4.  In particular, many users (not least Magnus and
> Thomas) don't just do proofs in HOL but they develop bigish
> libraries for doing automated proofs.

Actually, I don't think HOL Light would be the place to start
something like that.  Its support for persistence requires the use of
OS specific check-pointing.  Indeed, the latest versions of Linux
apparently break the standard tool, meaning that John has to run HOL
Light inside a virtual machine installation of an old version of
Linux.  (I have this from a student of mine who e-mailed John a little
while ago; I hope I'm not spreading false scuttlebutt.)  HOL Light
also has clarity rather than efficiency as a design desiderata, which
is precisely the opposite of what we want (it has a clean kernel,
including use of lists for storing assumptions, etc).  Of course, the
pleasant surprise with HOL Light is that it still performs well.

I would also argue against porting to OCaml: having just one
implementation of a language is not a healthy place to be in,
particularly if, in this case, the implementation is by researchers
who will either continue to develop the language, or give it up.  (I
get enough grief as it is with backwards incompatibilities, think how
much worse it would be if the language changed underneath you.)  I'm
not really serious about F# (no-one can really provide the resources
to make the port), but it is at least a MS product.

> The current suggestions seem sound to me i.e.

> * Push for a new release of Mosml (or, looking more likely, release
> our own version).  This would provide the latest patches and bug
> fixes and should fix most of the SML non-compliance.

The non-compliance is just the Basis library.  There are also problems
with the runtime when programs/theories get too large.  But I agree
that this would be nice.  Does anyone have some time to give to this?
I don't, not at the moment anyway.  Perhaps in October...

> * Continue to try and get the standard kernel working with Poly/ML.
> Then avoid using the experimental kernel, except for it's intended
> "experimental" purpose.

Alternatively, make the experimental kernel as it now stands the
"standard".

> * Avoid writing non-standard ML and the use of non-standard libraries.
> (Although I guess this is not so easy when the compiler doesn't
> enforce this upon you.)  If necessary, extend libraries provided by
> src/portableML.

There is precious little of this in the system as it stands.

> * Push for fixes to Poly/ML and continue to improve support for
> working with Poly/ML i.e. follow Magnus' suggestions in that area.  I
> would also like to see the online help system working with Poly/ML.

The online help system *is* working in Poly/ML.

> * If improvements are made, and things work out with Poly/ML, then
> possibly abandon Mosml in the long term.  One could then optimise
> more for Poly/ML and maybe eventually *carefully* use Poly/ML
> specific features e.g. threads.

If we wanted to use system-specific features, then we should hide them
in a portableML like setup.  Again, there is nothing really of this
nature at the moment.  If you look at portableML, most of it is
implemented in terms of the Basis library.

Incidentally, in dropping mosmlyac and mosmllex, we have necessarily
embraced functors, because they are used by mlyacc and mllex (which
are portable, unlike mosmlyac and mosmllex).  We are thus using pretty
much all of SML.

Michael.