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; Mon, 6 Jun 1994 08:23:40 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25213; Mon, 6 Jun 1994 01:05:05 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25209; Mon, 6 Jun 1994 01:04:39 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Mon, 6 Jun 1994 08:59:28 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <11830-0@i80fs2.ira.uka.de>; Mon, 6 Jun 1994 09:06:02 +0200 Date: Mon, 6 Jun 94 9:06:02 EDT From: reetz To: info-hol@leopard.cs.byu.edu, byu@twu.ca Subject: RE:Linux and HOL Message-Id: <"i80fs2.ira.832:06.05.94.07.06.07"@ira.uka.de> >Has anyone run HOL on Linux? Yes, me. But I'm running HOL90.6 (!not! hol88) on Linux, Slackware 1.2.0, kernel 1.0.8. However, you have to be aware of a bug in the unsupported version of SML/NJ 0.93 for Linux: getWD() does not work properly. As E. Gunter noted before, you can get around this problem by supplying the HOLDir - path directly to the script make_hol. I'm running Xholhelp on Linux, too. You just have to recompile it. I used gcc 2.5.8. You only need to set the help path, then run the installation script as described. Be aware that for Slackware 1.2.0, you have to set the path to cpp for imake, otherwise the installation script will fail because it won't find cpp. Ralf. (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)