Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: mikef@dcs.ed.ac.uk, info-hol@ted.cs.uidaho.edu
In-Reply-To: Michael Fourman's message of Thu, 24 Jun 1993 17:39:07 +0200 <14093.9306241539@rough.dcs.ed.ac.uk>
Subject: HOL portability
Message-Id: <93Jun24.220822met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 24 Jun 1993 22:08:21 +0200


In response to Mike Fourman's note, let me express my unqualified
admiration for anyone who writes and maintains an SML compiler: it's a
bloody difficult language. In my opinion, Dave Matthews has not received
the credit he deserves for the PolyML compiler; it is a fine piece of
work, and hol90 certainly should be re-ported to it. Any volunteers?

> Last time we were able to make a direct comparison at AHL, HOL90
> performance on our 32Mbyte Sparc machines under Poly and NJ was 
> roughly comparable. If Konrad had been able to keep HOL90 compatible 
> with *Standard* ML, then users could easily determine what works best 
> for them.

Indeed, but I wonder what Mike's definition of "compatible" is? If he
means "expressed solely in the language given in the Definition", that's
not possible: I need "use" ("load" to hol88ers) to even begin to build
the system, but "use" is not in the Definition. (To avoid "use", I
suppose I could sit at the unix level and "cat" all the hol90 source
files through a pipe into the compiler, but that's lame.) Another
example: hol90 needs timestamps for security in the implementation of
theories, but the Definition is silent about such things as system
calls.

SML was intended to meet the requirements of both theorists and system
developers. The Definition does not meet the requirements of the second
group. In a such a vacuum, it's no wonder that different support
libraries spring up around different implementations. We are reduced to
hoping (rather than being able to demand) that each new implementation
of SML provide an adequate support library.

< A joke starts here

    "Bless me Father, for I have sinned; I strayed outside of the SML
     Definition 3 times this week."

    "You are forgiven my child; as penance say 3 Hail Marys and read
     the X documentation."

Now it is over >

> It is a pity if HOL90 only works with one particular implementation of
> Standard ML, since other implementations (available now or under
> development) may be more efficient.

Well, yeah I agree with you, although I think efficiency is not as
important as portability between architectures.


I suspect that PolyML is an unknown quantity to most of the readers of
info-hol. Perhaps Mike Fourman could give us some particulars on it?


Konrad.