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
