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. Alex