[isabelle-dev] Sledgehammer renaming
makarius at sketis.net
Wed Jan 13 17:57:21 CET 2010
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.
More information about the isabelle-dev