Opened 10 years ago

Closed 10 years ago

#387 closed defect (fixed)

Preferences lost when prover restarted

Reported by: Makarius Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc: makarius@…


When starting the prover process, defaults are received, but current values on the PG side are not sent.

This means, users cannot work with persistent prefs at the moment.

Attachments (1)

repeat-hasprefs-bug.patch (716 bytes) - added by David Aspinall 10 years ago.
Simple patch to prevent loss of settings

Download all attachments as: .zip

Change History (7)

comment:1 Changed 10 years ago by Makarius

This appears to be some collateral damage caused by the attempt to upgrade PGIP to support floats.

In ProofGeneral-4.1pre101216 it appears to work, i.e. that is the version we will take as a basis for Isabelle2011.

comment:2 Changed 10 years ago by David Aspinall

Can you give a repeatable test case please?

comment:3 Changed 10 years ago by Makarius

Looking at the *isabelle* buffer, there is never a setpref message as it used to be.

Getting into this situation should be trivial, e.g. start prover, change settings, save settings, stop prover, start prover.

In ProofGeneral-4.1pre101216 it works better, but might require a few rounds of change settings, save settings until it is really persistent.

comment:4 Changed 10 years ago by David Aspinall

Status: newaccepted

Confirmed: nothing to do with the float upgrade, rather it stems from trying to smoothly support both dynamic configuration settings (potentially varying with each prover invocation) and static ones which are declared directly in the elisp.

The CVS server seems to be having problems at the moment, but a one-line workaround patch is to remove the call to makunbound on line 77 of proof-compat.el. This call has the bad effect of losing user customizations when the prover gets started for the second time in an Emacs session.

I have a more sophisticated fix for PG 4.1, for when CVS is back up, but suggest you take that simple one-line fix for Isabelle2011's PG.

The smarter fix allows for changing sets of preferences between different Isabelle invocations --- I'm not sure if that ever happens (perhaps with a change in object logic?). If it does, and the user has configured a setting which is not in the new invocation, startup may generate an error. (Workaround: new Emacs, don't change such settings...)

Changed 10 years ago by David Aspinall

Attachment: repeat-hasprefs-bug.patch added

Simple patch to prevent loss of settings

comment:5 Changed 10 years ago by David Aspinall

Summary: Preferences not sent to prover on startupPreferences lost when prover restarted

comment:6 Changed 10 years ago by David Aspinall

Resolution: fixed
Status: acceptedclosed

More elaborate fix in CVS now. The CVS version allows for different prover invocations to use different sets of dynamic settings (i.e., those returned from PGIP askprefs messages), but only the most recent set of settings will be saved/reset by Isabelle -> Settings -> Save Settings.

As an additional improvement, the revised code only sends setpref commands for settings which are different from the prover defaults.

Note: See TracTickets for help on using tickets.