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

On Sun, 10 Nov 2013, Gottfried Barrow wrote:

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

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.

That is an interesting corollary of sledgehammer as "query operation".

The sledgehammer invocation is associated with a "document overlay", based on the static command 'theorem', and it remains there until you invoke it differently. So when you edit before that command, it is re-checked together with its sledgehammer overlay.

This gives the effect of "run on its own". The "Cancel" button is not sufficient to remove the potential sledgehammer run, it only refers to the current dynamic execution of it. So to dispose sledgehammer permanently, you need to apply it elsewhere (e.g. outside a proof context), or undock the panel.

There's also no persistence in the "Provers" field.

The persistence is in the history of the text field. This is also useful to "park" several sets of options that are commonly used.


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