Return-Path: Delivery-Date: Received: from lal.cs.byu.edu (actually leopard.cs.byu.edu !OR! info-hol-request@lal.cs.byu.edu) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 26 Sep 1994 15:40:15 +0100 Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA03500; Mon, 26 Sep 1994 08:26:08 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from eagle.eng.warwick.ac.uk by lal.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA03496; Mon, 26 Sep 1994 08:26:02 -0600 Received: from eng.warwick.ac.uk by eagle.eng.warwick.ac.uk with SMTP id PAA06744; Mon, 26 Sep 1994 15:20:25 +0100 From: es774@eng.warwick.ac.uk Date: Mon, 26 Sep 94 15:20:23 BST Message-Id: <2472.9409261420@eng.warwick.ac.uk> To: info-hol@lal.cs.byu.edu Subject: hol-486-586 To: Info-hol From: Karim; es774@eng.warwick.ac.uk Subject: Porting HOL on 386 based machine. Hi all, I think I have successfully ported HOL on a 386 based machine (not on DOS operating system). It took me about nine months of searching (part time) to get this far I don't how long it will take to finish my PhD. I am now running hol on a shareware operating system (unix variant). The machine has eight megs of RAM. It is not as much slow as the sun 3 machine. In fact on DX-2/66 it is as fast as an sparc 1 machine. If I have another 8 megs of RAM I will be able to compile HOL in one hour instead of three hours and a bit. I am using latest version of AKCL compiler. I have not seen any incompatibilities with the Libraries so far. I am using it for last couple of months. With present first intel processor it is possible to run hol at a comparable speed of that of an sparc. If any of you are interested I can provide you further information. I think it is now possible to give access to hol to a wider audience including university/college lecturer, students, industry and so on. Thank you very much for a wonderful tool (although it took 40 floppy disk to copy hol and the operating system but it was worth it). Karim. Thank you.