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.
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-184.108.40.206 / 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and