Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)



On Tue, 18 Sep 2012, René Neumann wrote:

Am 05.09.2012 16:23, schrieb René Neumann:
Am 05.09.2012 15:42, schrieb Makarius:
As far as I know this "feature" of Proof General has been always there
in the 4.x line of versions.  You should put this on the regular Proof
General tracker and maybe also raise some attention on the Proof General
proofgeneral-devel mailing list.

http://proofgeneral.inf.ed.ac.uk/trac/ticket/452

- René


Humm. The ProofGeneral-Devs have now closed this issue with a "it's
Isabelle's fault"-message. So who is correct here?

That was "da", i.e. David Aspinall himself. And he did not formulate it that way -- assigning the blame or fault to someone or some of the systems involved is irrelevant for resolving the issue. The code used here on the Isabelle side is by David Aspinall himself anyway, going back to his PGIP experiments with Isabelle around 2005/2006.


I think the deeper probelm is a misunderstanding what the PGIP messages "askprefs" vs. "setpref" mean, notably the "default" field of "askprefs".

In classic ProofGeneral-3.7.1.1 / XEmacs 21.4, the prover would report static defaults stemming from "askprefs", and Proof General react with further "setpref" messages to adapt to the dynamic values on either side, such that the persistent preferences from Emacs are transferred to the prover at run time.

In PG 4.0 or so, it would depend on the Emacs version if this worked out or not.

Now in PG 4.1 with GNU Emacs 23.x it seems that it never works: I see only the initial askprefs by the prover, without any readjustments by PG. This means that more basic things like quick-and-dirty also don't work, i.e. it is off (the usual default of Isabelle), but Proof General displays it as on, while leaving it de-facto off.

PG 4.2 is about to be released soon, so this is the chance to disentangle PGIP preference messages.


This discussion should probably continued on the above PG trac thread or the proofgeneral-devel mailing list, which is dangerously unpopulated in relation to the number of people who have now publicly confessed that they are still using Proof General Emacs.


	Makarius


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