Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <4906.9410110910@frogland.inmos.co.uk>
Subject: Re: little things that make HOL unfriendly....
To: windley@leopard.cs.byu.edu (Phil Windley)
Date: Tue, 11 Oct 1994 10:10:44 +0100 (BST)
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <9410101714.AA01120@jaguar.cs.byu.edu> from "Phil Windley" at Oct 10, 94 11:14:44 am
Content-Type: text
Content-Length: 1330

Phil Windley has said:
> This may not be something for HOL 2000, it may be something more suited for
> HOL96, but...
> 
> One thing that bothers me is that new_theory won't overwrite an existing
> theory file.  So, most of us regularly do:
> 
> system `/bin/rm -f theory.th`;;
> 
> new_theory `theory.th`;;
> 
> Once you know it, its not bad, but teaching it to beginners is just one
> more nitpicky detail that they have to know.  This one small change is not
> going to make HOL significantly better, but lots of them would.  
> 
> What little things about HOL bother you?  

A little thing about SMLofNJ that bothers me is that the method
described  above hits a "feature" in SMLofNJ which causes it to need
another image the size of the existing SML session to run rm in! As a
result I used to find that it always failed so I had to resort to
deleting the file by hand!

Actually, a quick look in the SMLofNJ sources shows that there is
a function:

	System.Unsafe.SysIO.unlink

which already deletese files without spawning off a shell.
 
--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."