[isabelle-dev] [isabelle] the sound of a sledgehammer

[Lawrence Paulson]

I would like to brainstorm some ideas for how to do sledgehammer in jEdit, but for this we need to move to the development mailing list.

One problem with the current approach is that one actually types "sledgehammer" in the proof document. That isn't how the document model is supposed to work, because it fixes on one current place, and the text you type doesn't actually belong there anyway.

In a dream scenario, one might imagine opening a document containing a number of occurrences of "sorry", and each one of these occurrences would be given to counterexample finders and to sledgehammer, without any specific user intervention. Then somehow any counterexamples or proofs that were found would be noted somehow, and the user could inspect these.

I recognise this idea isn't even half baked. But I know that you want to look at these problems differently from just saying, "how did it work in Proof General"? And the idea of having a whole bunch of gaps checked (as it were) simultaneously is very appealing.

Larry

On 14 Feb 2013, at 12:58, Makarius <makarius at sketis.net> wrote:

> On Thu, 14 Feb 2013, Lawrence Paulson wrote:
> 
>> The entire internal architecture supports this background execution, so it should be possible.
> 
> Which version of the architecture do you mean?  Fabian Immler and myself rewrote most of it from scratch in 2008, to make it work without Unix process fork, and thus on Cygwin for the first time.  Later Jasmin also rewrote it again.
> 
> All of that is for the TTY loop, though.  It has to be re-integrated into the native Isabelle document model, and this is where I am stuck for several years for no particular technical reasons, just social ones.
> 
> 
> 	Makarius