Re: [isabelle] Isabelle2013-1-RC4 available for testing



Hi,

After I've run Sledgehammer once in the panel by clicking "Apply", it will run on its own, and here is the description:

The following is in the file Scratch.thy, in a new Cygwin installation in which I've changed no options.

theory Scratch
imports Complex_Main
begin

theorem "A = A"
oops
end

I place my cursor after "A = A", I click "Apply", Sledgehammer runs, and it returns "Try this: by metis (1 ms)" for e, spass, remote_vampire, and that I need to change "Z3_NON_COMMERCIAL" to yes.

I place my cursor at the empty line before "theorem", hit the space bar, Sledgehammer runs again on its own, returns the same results, and it terminates like it should.

So, I can edit anything after "A = A", but if I make any edits before "theorem", it runs on its own, even if I click on a proof so that it's inserted. This happens every time after I exit and restart jEdit, and there are no other files open.

There's also no persistence in the "Provers" field. The "Previously entered strings" is always empty, no matter how many times I've edited the field. I don't care about that. I'm just reporting it.

Regards,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.