[isabelle-dev] Sledgehammer renaming
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
[isabelle-dev] Sledgehammer renaming
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
[isabelle-dev] Sledgehammer renaming
Hi, Tobias asked me to look at Sledgehammer and see if it would be possible to improve the relevance filter and the proof reconstruction to get a better success rate. As a first step towards that, I was thinking of refactoring the Sledgehammer code. In particular: 1. Put all the Sledgehammer files in HOL/Tools/Sledgehammer (and remove the res_ prefixes and give clearer names, e.g. fact_filter.ML instead of res_atp.ML). 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. Does anybody have objections/comments? Jasmin
[isabelle-dev] Sledgehammer renaming
On Wed, 13 Jan 2010, Jasmin Blanchette wrote: Tobias asked me to look at Sledgehammer and see if it would be possible to improve the relevance filter and the proof reconstruction to get a better success rate. As a first step towards that, I was thinking of refactoring the Sledgehammer code. In particular: 1. Put all the Sledgehammer files in HOL/Tools/Sledgehammer (and remove the res_ prefixes and give clearer names, e.g. fact_filter.ML instead of res_atp.ML). 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. As usual when changing things, one needs some understanding of the history and current state of the sources in question. By looking at the Mercurial history one can easily see who has introduced things and who has cared enough about it to rework them at some point. The ATP manager is relatively new (and clean), mostly due to Fabian Immler and myself. In short, I do not see any good reason for reorganizations here. The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. There are also papers and talks that allude to this ATP stuff. Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. Makarius
[isabelle-dev] Sledgehammer renaming
Hi Makarius, Am 13.01.2010 um 17:57 schrieb Makarius: The ATP manager is relatively new (and clean), I have to disagree here -- but not with the new part. I find it dubious that ATP_Manager is based on ATP_Wrapper and not the other way around. As a result, adding a new ATP (besides E, SPASS, and Vampire) means editing two files instead of just one. This is a sign to me that the design can be improved. In short, I do not see any good reason for reorganizations here. In addition to the reason named above, I'd like to invoke other services than ATPs on goal states and generate a message after running a certain time, asynchronously. ATP_Manager provides such an architecture -- and by doing minor modifications, it could be used by other diagnosis tools. 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.) The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. Yes. And I would of course change them all. There are also papers and talks that allude to this ATP stuff. This cannot be a good reason for not changing things. I'm sure Larry's and Tobias's old papers are full of lies :) Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. The word assistant is not cast in stone either -- it was merely the result of a brain storming session with Florian and Sascha. I hadn't thought of the confusion with proof assistant. Other names are possible, like diagnosis tool, hinter, wizard, sidekick, etc. We have plenty of time to think about it (I'm not going to touch anything in the coming few weeks, or before there's a consensus). Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. For now I was thinking of more or less a one-to-one mapping between the current files and the new files, with a few exceptions (e.g. the clausify stuff and the meson tactic don't belong in res_axiom.ML). Further improvements could come later. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. That's something that will have to change. Regressions tests for Sledgehammer are tricky, because it tends to be fragile (adding a theorem to HOL can affect its results), but the overall performance of the tool should be fairly stable. Sascha now has a suite of tests that can run for about 4 hours (as a spin-off of the Judgement Day paper), which could form the basis of such a benchmark suite. Jasmin
[isabelle-dev] Sledgehammer renaming
PS Since I suggested to Jasmin to work on s/h, I obviously welcome his initiative. It is important that we have one person who has the time and the responsibility, just like other people feel responsible for fun etc. Tobias Jasmin Blanchette wrote: Hi Makarius, Am 13.01.2010 um 17:57 schrieb Makarius: The ATP manager is relatively new (and clean), I have to disagree here -- but not with the new part. I find it dubious that ATP_Manager is based on ATP_Wrapper and not the other way around. As a result, adding a new ATP (besides E, SPASS, and Vampire) means editing two files instead of just one. This is a sign to me that the design can be improved. In short, I do not see any good reason for reorganizations here. In addition to the reason named above, I'd like to invoke other services than ATPs on goal states and generate a message after running a certain time, asynchronously. ATP_Manager provides such an architecture -- and by doing minor modifications, it could be used by other diagnosis tools. 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.) The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. Yes. And I would of course change them all. There are also papers and talks that allude to this ATP stuff. This cannot be a good reason for not changing things. I'm sure Larry's and Tobias's old papers are full of lies :) Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. The word assistant is not cast in stone either -- it was merely the result of a brain storming session with Florian and Sascha. I hadn't thought of the confusion with proof assistant. Other names are possible, like diagnosis tool, hinter, wizard, sidekick, etc. We have plenty of time to think about it (I'm not going to touch anything in the coming few weeks, or before there's a consensus). Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. For now I was thinking of more or less a one-to-one mapping between the current files and the new files, with a few exceptions (e.g. the clausify stuff and the meson tactic don't belong in res_axiom.ML). Further improvements could come later. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. That's something that will have to change. Regressions tests for Sledgehammer are tricky, because it tends to be fragile (adding a theorem to HOL can affect its results), but the overall performance of the tool should be fairly stable. Sascha now has a suite of tests that can run for about 4 hours (as a spin-off of the Judgement Day paper), which could form the basis of such a benchmark suite. Jasmin ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer renaming
On Wed, 13 Jan 2010, Tobias Nipkow wrote: PS Since I suggested to Jasmin to work on s/h, I obviously welcome his initiative. It is important that we have one person who has the time and the responsibility, just like other people feel responsible for fun etc. Yes, responsibility is the key thing here, not consensus. If Jasmin wants to take over the full responsibility of Slegehammer, and I will never have to worry about it, I would be relieved of many burdens. (Most of them unseen in the background.) Part of this is to keep everything going on all of our official platforms. This state has not yet been achieved for nitpick, where Jasmin *is* fully responsible right now. Makarius
