Email Gateway (Aug 19 2022 at 08:39): Email Gateway (Aug 19 2022 at 08:39):From: René Neumann <rene.neumann@in.tum.de>
Humm. The ProofGeneral-Devs have now closed this issue with a "it's
Isabelle's fault"-message. So who is correct here?
Email Gateway (Aug 19 2022 at 08:39):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 08:39):From: René Neumann <rene.neumann@in.tum.de>
Am 19.09.2012 14:41, schrieb Makarius:
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.
So in essence Isabelle states some setting being defaulted to, but
relies on an explicit message to actually set it to this default? And PG
4.x does not send this message anymore?
This discussion should probably continued on the above PG trac thread
So I may paste your message there?
Email Gateway (Aug 19 2022 at 08:39):From: Makarius <makarius@sketis.net>
I don't know for sure. This part of PGIP is due to David Aspinall, both
the older and newer behaviour.
Makarius
Email Gateway (Aug 19 2022 at 08:39):From: René Neumann <rene.neumann@in.tum.de>
Ok - I skimmed the sources in Isabelle. And as far as I see it, the
defaults of boolean preferences are the actual values of the variables.
Hence this should be ok. BUT: Some preferences are set in an
Unsynchronized.setmp block which cancels this assumption.
So probably the easiest solution would be to just cycle through the
preferences on PG-startup and set them explicitly to their default.
This I did in the attached patch and it fixes the issue :). It is
probably saner to actually ensure defaults are set, instead of relying
on the other side to explicitly set them.
P.S.: I'm not sure, whether the call of 'enforce_preference_defaults' is
actually at the right place in the whole startup process. So it probably
needs to be moved around.
isabelle-enforce-defaults.patch
Email Gateway (Aug 19 2022 at 08:40):From: Makarius <makarius@sketis.net>
Yes, these setmps are the right thing in terms of the classic
interpretation of PGIP askprefs/setpref messages -- whatever that was
exactly. You still have that classic behaviour in ProofGeneral-3.7.1.1,
which is still the standard version of many Proof General users.
Before changing anything on the Isabelle side, I need an explanation if
PGIP has changed in recent years, or if it is just an accident of the
PG-4.x line.
This is particularly relevant since I am about to revisit the PGIP
preferences implementation soon, to unify it with the standard Isabelle
options/preferences mechanism that will be in the next release. Otherwise
the "fix" will become loose again and just fall off.
Makarius
Email Gateway (Aug 19 2022 at 08:43):From: René Neumann <rene.neumann@in.tum.de>
Hi,
(some of) the options set for Isabelle in ProofGeneral (like "Auto Solve
Direct", "Auto Quickcheck") are not active, even though they are
enabled. I don't know whether this bug lives in PG or in Isabelle...
Anyways: A normal workaround is to disable and enable these options
again in the menu -- which is cumbersome.
Hence: Find attached an Elisp-function 'isabelle-repair', which does
this toggling for you after Isabelle startup. Perhaps somebody finds
this useful :)
This function can then be called for each parameter that matters for you:
(isabelle-repair "auto solve direct" "tracing")
(isabelle-repair "auto quickcheck" "tracing")
Probably, this could be expanded to repair every option that has the
problem, but I don't know on how to collect them.
Email Gateway (Aug 19 2022 at 08:43):From: Makarius <makarius@sketis.net>
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.
I am myself no longer involved in Proof General maintenance since almost 1
year. Larry Paulson and Jasmin Blanchette have taken over
responsibilities to organize and motivate continued support for that
classic Isabelle interface.
Right now the few active people on the proofgeneral-devel mailing list
have switched into PG 4.2 release mode, so it is the right time to make
some progress, not just keeping the status quo (where the above issue is a
well-known part of).
Makarius
Email Gateway (Aug 19 2022 at 08:43):From: René Neumann <rene.neumann@in.tum.de>
Am 05.09.2012 15:42, schrieb Makarius:
On Wed, 5 Sep 2012, René Neumann wrote:
(some of) the options set for Isabelle in ProofGeneral (like "Auto
Solve Direct", "Auto Quickcheck") are not active, even though they are
enabled. I don't know whether this bug lives in PG or in Isabelle...Anyways: A normal workaround is to disable and enable these options
again in the menu -- which is cumbersome.I am myself no longer involved in Proof General maintenance since almost
1 year.
I know this. My mail was just in line of "I coded a workaround; whoever
might need it, can use it".
Right now the few active people on the proofgeneral-devel mailing list
have switched into PG 4.2 release mode, so it is the right time to make
some progress, not just keeping the status quo (where the above issue is
a well-known part of).
This is of course reasonable. I'll see what kind of awareness can be raised.
Email Gateway (Aug 19 2022 at 08:43):From: René Neumann <rene.neumann@in.tum.de>
http://proofgeneral.inf.ed.ac.uk/trac/ticket/452
Last updated: Nov 21 2024 at 12:39 UTC