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, 14 Apr 1994 19:48:57 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14869; Thu, 14 Apr 1994 12:30:31 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from ninet.research.att.com by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA14865; Thu, 14 Apr 1994 12:30:29 -0600 Received: by ninet.research.att.com; Thu Apr 14 14:27 EDT 1994 Received: by hunny.research.att.com (/\==/\ Smail3.1.25.1 #25.11) id ; Thu, 14 Apr 94 14:27 EDT Received: by tiree.research.att.com (/\==/\ Smail3.1.25.1 #25.1) id ; Thu, 14 Apr 94 14:27 EDT Message-Id: Date: Thu, 14 Apr 94 14:27 EDT From: elsa@research.att.com (Elsa Gunter) To: info-hol@leopard.cs.byu.edu Subject: hol90 on a PC under LINUX Dear HOL/PC community: If you would consider switching from hol88 to hol90 and are a PC-LINUX user, now would be a good time to do so. There is a compressed executable version of SML/NJ v0.93 that runs on PC running LINUX which may be had via ftp from research.att.com:/dist/ml/hol90/sml.i386.Z There is one small inconvenince (bug) with this version. The function System.Directory.getWD is broken. This function is used by two functions in hol90. The first place is in deciding what the HOLdir is. You can easily get around this by using the -d option to make_hol to specify the HOLdir. Then getWD want get called. The second is in the definition of Lib.pwd. You can get around this just by not using it. On the other hand, if you really wish to have a working pwd, below is a slow version that will work. I have build hol90.6 on a Dell PC running Linux 1.0.5, and I have found it to work great (much better than a Sparc 2). ---Elsa L Gunter elsa@resaerch.att.com fun pwd () = let val (I,O) = execute ("/bin/pwd",[]) val dir = input_line I; val _ = close_in I val _ = close_out O in substring (dir, 0, size dir - 1) end