Email Gateway (Aug 18 2022 at 17:35): Email Gateway (Aug 18 2022 at 17:35):From: Brian Huffman <brianh@cs.pdx.edu>
Hello,
I have been frustrated recently by ProofGeneral's failure to preserve
the Isabelle settings that I have selected and saved.
The Isabelle options "Auto Solve Direct", "Auto Quickcheck", and "Eta
Contract" are all enabled by default in Isabelle2011. I do not ever
want to use any of these features, so I have unchecked them in the
Isabelle > Settings menus in ProofGeneral, and saved them to my .emacs
using Isabelle > Settings > Save Settings. I can see that the settings
were saved properly, since the following lines appear in my .emacs
file, in the custom-set-variables section:
'(isar-display:eta-contract nil)
'(isar-tracing:auto-quickcheck nil)
'(isar-tracing:auto-solve nil)
'(isar-tracing:auto-solve-direct nil)
When I start a new Isabelle session in ProofGeneral, these settings
are all disabled, as they should be. However, if I stop the Isabelle
process with C-c C-x, and then start it again, these options magically
turn themselves on! It is very annoying to have to dig through 3
levels of menus to turn each one of them off again. The "Auto
<whatever>" options are especially problematic because they can slow
down theory processing so much.
Has anyone else experience a similar problem? And is there any way to
fix it, short of changing the hardwired default settings in the
Isabelle sources, and recompiling all my heap images?
Email Gateway (Aug 18 2022 at 17:35):From: Makarius <makarius@sketis.net>
See also http://proofgeneral.inf.ed.ac.uk/trac/ticket/387
As is recorded there, I've used ProofGeneral-4.1pre101216 for
Isabelle2011, which appeared to work in the Emacs platforms tested at that
time. Later further complications showed up, so there might be more to say
than seen in the trac thread.
Makarius
Email Gateway (Aug 18 2022 at 17:36):From: Brian Huffman <brianh@cs.pdx.edu>
Yes, I should have said that I was using 4.1pre110112. However, I just
tried reverting to 4.1pre101216, and I get the exact same behavior as
far as I can tell. Using "Save Settings" doesn't change any relevant
lines in my .emacs file. I am using PG with GNU Emacs 23.2.1.
For now, I think I will be recompiling my Isabelle2011 heap images
with different hardwired defaults.
Last updated: Apr 18 2024 at 20:16 UTC