Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <20181-0@swan.cl.cam.ac.uk>; Thu, 14 Mar 1991 11:26:54 +0000 Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk with SMTP inbound id <8455-0@sun2.nsfnet-relay.ac.uk>; Thu, 14 Mar 1991 11:24:56 +0000 Received: from iris.ucdavis.edu by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP id aa06032; 14 Mar 91 10:58 GMT Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.4.0) id AA07023; Thu, 14 Mar 91 03:15:42 -0800 Received: from iraun1.ira.uka.de by clover.eecs.ucdavis.edu (5.59/UCD.EECS.1.11) id AA10742; Thu, 14 Mar 91 03:17:01 PST Message-Id: <9103141117.AA10742@clover.eecs.ucdavis.edu> Received: from i80s12.ira.uka.de by iraun1.ira.uka.de id aa24502; 14 Mar 91 12:11 MET Date: Thu, 14 Mar 91 12:07:54 MET From: Ramayya Kumar To: info-hol@edu.ucdavis.clover Subject: Problems installing HOL 1.12 Has anyone been able to successfully install the new version of HOL using either SUN CL 3.0 or Franz Lisp Version 38.92. I have already sent a list of errors to Phil Windley as regards the CL 3.0 installation. I have tried some patches but I do not get beyond the installation of hol-lcf. The PPLAMB theory can be created but bool.th cannot be created as a call to new_parent in file mk_bool.ml reports "new_parent -- PPLAMB theory damaged". The Franz Lisp version does better in that, the theories PPLAMB, bool, ind and BASIC-HOL are created. However, the compilation of the file ml/hol-syn could not be done as "axiom" is reportedly an unbound or non-assignable variable. I tried to include "lisp `(load "lisp/f-thyfns")`;;" in the Makefile but it doesn't work either. The error then reported is "evaluation failed axiom -- bool is not an ancestor". Before I start hacking further patches I would wait for some HOL experts to give me an advice. Thanks, Kumar