[isabelle-dev] Sledgehammer renaming

[Jasmin Blanchette]

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