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, 31 Oct 1994 20:47:26 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA09317; Mon, 31 Oct 1994 13:43:03 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from [130.209.240.50] by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA09313; Mon, 31 Oct 1994 13:43:00 -0700 Received: from hawaii.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Mon, 31 Oct 1994 20:34:12 +0000 To: Peter Bumbulis Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Re: problems with sem.ml in contrib/prog_logic92 In-Reply-To: Your message of "Wed, 26 Oct 1994 21:47:37 -0400." <94Oct26.214748edt.763@csg.uwaterloo.ca> Date: Mon, 31 Oct 1994 20:34:00 +0000 From: Tom Melham Message-ID: <"swan.cl.cam.:085520:941031204816"@cl.cam.ac.uk> > I'm having problems make'ing contrib/prog_logic92. Doing a "make clobber" > followed by a "make all" stops with a lisp error in sem.ml: > > ... > Theorem lub_first autoloading from theory `exseq` ... > lub_first = |- !Ch. chain $<=| Ch ==> (first(lub $<=| Ch) = first(Ch 0)) > > > Error: FUN%3009%1245 is invalid as a function. > ... > > I've tried it wigh a couple of versions of HOL88/2.02 (Allegro/SunOS and > gcl/Linux) with similar results (both versions of HOL have been rebuilt from > scratch.) Any suggestions as to where I should start looking (the > accompanying documentation suggests that it worked with HOL88/2.01.)? Hard to say what's happening here. Contrib code is not supported, so I'd suggest you contact the original author. Otherwise, you could start by loading the file into an interactive session and then try to execute the offending tactic line by line. Perhaps you'll spot a looping rewrite, or some other obvious error... Best wishes, Tom