[isabelle-dev] Sledgehammer renaming

[Makarius]

On Thu, 14 Jan 2010, Alexander Krauss wrote:

> Makarius wrote:
>> On Wed, 13 Jan 2010, Jasmin Blanchette wrote:
>>> 2. Generalize "atp_manager.ML" so that it can manage arbitrary 
>>> "assistants", which are tools that take a goal and produce a message -- 
>>> not just ATPs -- and rename it "HOL/Tools/assistant.ML".
>
> Makarius wrote:
>> Although the "ATP" manager can technically manage almost everything, 
>
> Actually having such an "everything_manager", which deals with all the 
> trouble of running things asynchronously would be an important thing. At 
> some point I will also need this functionality, for connecting to 
> external termination provers.
>
> Maybe a UI architecture which is inherenetly asynchronous will provide 
> this anyway and be even more general... But so far, atp_manager is the 
> best we have, and it would be nice if it could be used for other tools, 
> too.

This "everything_manager" will just be the Isar toplevel.  I keep talking 
about these things for about 2 years already, and there have been 
substantial progress recently, where I refrained from talking but made a 
few things actually work.  Many more needs to be done.

Since the general Isabelle/Isar system integrity is definitely my very own 
responsibility, prospective users need to wait until this is supported. 
(For Sledghammer it took more than one year until we had a version that 
was technically ready for prime time.)

People who have some experience with our development process know that 
there can be long delays, but in the end there is now alternative to doing 
things right.


 	Makarius