Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 24 Aug 1995 16:35:21 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA008617385; Thu, 24 Aug 1995 09:16:25 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from ra.abo.fi by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA008587379; Thu, 24 Aug 1995 09:16:19 -0600 Received: from aton.abo.fi (root@aton.abo.fi [130.232.18.1]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id QAA29183; Thu, 24 Aug 1995 16:42:23 +0300 Received: from aton.abo.fi (jgrundy@localhost [127.0.0.1]) by aton.abo.fi (8.6.10/8.6.10) with ESMTP id QAA17185; Thu, 24 Aug 1995 16:42:39 +0300 Message-Id: <199508241342.QAA17185@aton.abo.fi> X-Mailer: exmh version 1.6 4/21/95 To: John Harrison Cc: hol2000@leopard.cs.byu.edu Subject: Re: Paper available: "HOL Done Right" In-Reply-To: Your message of "Tue, 22 Aug 1995 12:59:28 EET DST." <"swan.cl.cam.:119490:950822115936"@cl.cam.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 24 Aug 1995 16:42:18 +0300 From: Jim Grundy INF Content-Transfer-Encoding: quoted-printable I enjoyed the paper and the motivations for the reorganisation. I'd like= to make a HOL2000 relavent point about the choice CAML light as the = implementation. I understand the choice of CAML light both on langauge syntax grounds but= also (and primarily) on performance grounds for small systems. It would = be nice if I people could get decent peformance out of 16M size machines. B= ut I don't think that marrying ourseves to CAML Light is the best way to go.= (My point will be that I don't think marrying ourselves to any specific = compiler is a good idea. HOL90's dependance on SML/NJ is also a problem.= ) I'd like to see HOL2000 written in something like SML + cpp mecros that c= ould contain lines like #ifdef NJ SML/NJ specific code #elseifdef Moscow Moscow ML specific code #elseif Poly Poly ML specific code #fi This is the sort of thing you see all over the place in C and LISP code t= hat attempts to be portable. You could run such code though cpp to get out code for your specific compiler. Hopefully the amount of compiler specif= ic code would be fairly small and the resulting system would be buildable un= der lots of different SML implementations and you could chode the one that su= its = you. i.e NJ if you have lots of memory, Moscow if you don't, Poly if you = are prepared to pay for performance. Doing it like this would mean restricting ourselves to only using that su= bset = of ML that is common to all the supported compilers, but maybe that subse= t is fairly large these days. Is this possible, or am I dreaming. Jim =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D =C5bo Akademi University | email: jim.grundy@abo.fi Department of Computer Science | phone: +358 (9)21 265-4034 Lemmink=E4isenkatu 14a | fax: +358 (9)21 265-4732 20520 Turku | www: http://www.abo.fi/~jgrundy/ FINLAND | time: UTC+2:00 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D