[isabelle-dev] Sledgehammer renaming

[Makarius]

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