[isabelle] permanently turning off "auto quickcheck", etc.



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?

- Brian





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