Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <20528-0@swan.cl.cam.ac.uk>; Fri, 13 Mar 1992 09:42:52 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13156; Fri, 13 Mar 92 01:31:44 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13152; Fri, 13 Mar 92 01:31:38 -0800 Received: from aldham.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <20111-0@swan.cl.cam.ac.uk>; Fri, 13 Mar 1992 09:34:17 +0000 Received: by aldham (5.57/SMI-3.0DEV3) id AA05143; Fri, 13 Mar 92 09:34:13 GMT Date: Fri, 13 Mar 92 09:34:13 GMT From: John.Carroll@uk.ac.cam.cl Message-Id: <9203130934.AA05143@aldham> To: info-hol@edu.uidaho.cs.ted Cc: John.Carroll@uk.ac.cam.cl Subject: HOL2.0 port to PC-compatibles I have recently finished porting HOL2.0 to PC-compatibles running Windows and Procyon Common Lisp. Performance looks to be good, for example a 33MHz 486 running faster than either a Sparc SLC or IPC under Allegro CL or AKCL. Here are some comparisons of run time for the multiplier benchmark: Machine Lisp Memory Window System Total Time -----------+--------------------+--------+---------------+----------- 33MHz 486 | Procyon | 8Mb | Windows 3.0 | 151.9 sec PC clone | | | | -----------+--------------------+--------+---------------+----------- Sparc SLC | Allegro | 16Mb | X (R4) | 214.4 sec -----------+--------------------+--------+---------------+----------- Sparc SLC | AKCL | 16Mb | X (R4) | 278.2 sec -----------+--------------------+--------+---------------+----------- Sparc IPC | Allegro | 16Mb | X (R4) | 174.9 sec -----------+--------------------+--------+---------------+----------- Sparc IPC | AKCL | 16Mb | X (R4) | 235.2 sec -----------+--------------------+--------+---------------+----------- SparcServ | Lucid | 64Mb | NONE | 102.7 sec -----------+--------------------+--------+---------------+----------- SparcServ | AKCL | 64Mb | NONE | 238.4 sec -----------+--------------------+--------+---------------+----------- Sparc2 | Allegro | 32Mb | SunView | 124.1 sec -----------+--------------------+--------+---------------+----------- Sparc2 | AKCL | 32Mb | SunView | 148.0 sec -----------+--------------------+--------+---------------+----------- DS5000/200 | KCL | 48Mb | NONE | 287.6 sec -----------+--------------------+--------+---------------+----------- Mac IIci | Procyon | 8Mb | Mac. Win. | 359.6 sec -----------+--------------------+--------+---------------+----------- I haven't had a chance to run the whole benchmark on a 386 machine, but extrapolating from running just the first part of it in a beta-release version of Procyon I estimate that an average 25MHz 386 would end up around the 320 second mark. Some details: the machine needs to be a 80386 or 80486 (may be SX or DX) with at least 5MB or memory -- preferably 8MB -- running Microsoft Windows 3 in 'enhanced mode'. Also needed is a copy of Procyon Common Lisp (costing 450 pounds sterling educational / 1500 pounds industry, obtainable from the address given below). The HOL system image occupies around 5MB disc space, and another 2MB is required for a minimal set of theory files etc. Judging from the benchmark figures, PC-compatibles look to be a cost-effective way of getting raw HOL power. (The 486 machine that I used cost under 2000 pounds). They also provide an inexpensive way (together with the new Macintosh notebook computers) of using HOL on a portable computer. One caveat, though, is that these are not UNIX machines so shell scripts, Makefiles etc will not work; in particular, building the HOL system from scratch requires a fair amount of manual intervention. Please e-mail me if you are interested in either a copy of the patches to HOL2.0 that are necessary and/or a ready-built copy of the HOL system image to go with a copy of Procyon that you are buying. John Carroll Cambridge University Computer Lab Procyon Common Lisp is sold by: Scientia Ltd., St. John's Innovation Centre, Cowley Road, Cambridge, CB4 4WS, UK; phone +44-223-421221, fax +44-223-421218.