[isabelle-dev] Sledgehammer renaming

[Makarius]

On Wed, 13 Jan 2010, Jasmin Blanchette wrote:

> I like the ATP_Manager's functionality; that's why I want to make it 
> more general and useful, rather than copy-paste it in every asynchronous 
> diagnosis tool. (E.g. today Nitpick can run asynchronously by specifying 
> an option, but there's no equivalent to "atp_kill" or "atp_messages".)

BTW, the whole ATP_Manager as a separate "manager" is only a workaround of 
the synchronous nature of Proof General.  As already pointed out many 
times, the Isar toplevel is only waiting for asynchronous interfaces to 
become usable.  Then any of this will be just a regular dignostic command, 
maybe with some indication about timeouts etc.


Moreover, here is a general rule of thumb of changing a big system 
successfully: At first the system is by definition always "right" the way 
it happens to be.  Then after more and more investigation into the status 
quo, understanding slowly emerges.  Only then there is the point to do 
some small amendments to make the system "really right" -- of course only 
until the next round of improvements.

Starting with "lets first get all this existing stuff right" quickly leads 
into desaster.


 	Makarius