Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199511210916.LAA23360@bruce.abo.fi>
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: better error messages in hol90? 
In-Reply-To: Your message of "Tue, 21 Nov 1995 09:35:13 EET."
             <"iraun1.ira.878:21.11.95.08.35.46"@ira.uka.de> 
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Date: Tue, 21 Nov 1995 11:16:44 +0200
From: Jim Grundy <jgrundy@ra.abo.fi>
Content-Transfer-Encoding: quoted-printable

Ralph says:
> I would strongly recommend not to depend on a however ``hacked''
> version of nj/sml for printing exceptions. The already existing
> dependency of hol90 on nj/sml only is painful enough.

I'd like to see a `hacked' version of nj/sml that would print out exeptions.
But, like Ralph, I would not like to see any dependancies introduced into HOL.
For me the ideal would be that HOL would run on both `hacked' and `unhacked'
versions of sml/nj, but would print out exeptions in the `hacked' version.
I certainly agree that the fewer dependancies we have on the nj implementation
the better.

Jim

=========================================================================
Åbo Akademi University          | email: jim.grundy@abo.fi
Department of Computer Science  | phone: +358 (9)21 265-4034
Lemminkäisenkatu 14a            | fax:   +358 (9)21 265-4732
20520  Turku                    | www:   http://www.abo.fi/~jgrundy/
FINLAND                         | time:  UTC+2:00
=========================================================================