Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id BAA23701; Fri, 5 Jan 1996 01:46:04 +0200 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA224976869; Thu, 4 Jan 1996 16:07:49 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: list Received: from puma.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA224946868; Thu, 4 Jan 1996 16:07:48 -0700 Received: from cs.byu.edu (localhost) by puma.cs.byu.edu (1.37.109.15/CS-Client) id AA295316875; Thu, 4 Jan 1996 16:07:55 -0700 Message-Id: <199601042307.AA295316875@puma.cs.byu.edu> To: Donald Syme Cc: info-hol@leopard.cs.byu.edu Subject: Re: A New Year hol90 update In-Reply-To: Your message of "Thu, 04 Jan 1996 21:45:02 +0100." Date: Thu, 04 Jan 1996 16:07:54 -0700 From: Kelly Hall On Thu, 04 Jan 1996 21:45:02 +0100 Donald Syme writes +-------------------- > That's all I can spot for now. Unfortunately I'm away for two weeks, > but I hope the above helps. Your changes *really* helped get me back on track. The only additions I'd make would be: a) change the "execute_in_env" call in 0/save_hol.sml to something else. I just commented out that stuff and assigned a string to "date". Lazy me. b) change the function "open_theory_outstreams" in 0/theory/io.sml since it seems the Io exception has changed somewhat (I changed the lines from "message = s" to "message = #name(s)". But now the fun really starts. Right after PRIM_HOL gets written, I get this error message: ------------------------------------- - HHH LL HHH LL HHH LL HHH LL HHH OOOO LL HHHHHHH OO OO LL HHHHHHH OO OO LLL HHH OOOO LLLL HHH LL LL HHH LL LL HHH LL LL HHH LL LL90.8 Created on Jan 4, 1995 using: Standard ML of New Jersey, Version 108.20, January 1, 1996 The library "PRIM_HOL" is loaded. uncaught exception Io: input failed on file sys01.sml with SysErr: Bad file number [] raised at: boot/IO/text-io-fn.sml:83.13-83.51 elaborate/frontend.sml:108.24 elaborate/frontend.sml:108.24 util/stats.sml:168.40 build/evalloop.sml:193.62 build/evalloop.sml:242.22-242.24 build/computil.sml:40.41 build/compile.sml:209.8 util/stats.sml:168.40 build/evalloop.sml:193.62 - ---------------------------- The filenames above don't seem to be part of hol90. So that sort of implies that this is a SML problem. Any ideas how I might get beyond this? BTW Donald: I owe you beverages in Abo for your help so far! I'm really out of my element in SML (and thus hol90). Thanks! Kelly