[isabelle-dev] Sledgehammer renaming

[Tobias Nipkow]

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