Opened 9 years ago

Closed 9 years ago

#452 closed defect (fixed)

Some Isabelle options enabled but not active

Reported by: Generic Isabelle user Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc: makarius@…


In PG 4.1 and 4.2pre120814 some options passed to the _running_ Isabelle instance (e.g. "Auto Quickcheck", "Auto Solve Direct") are enabled via config and are also been shown as enabled in the menu, but are not active, i.e. isabelle seems to not see them as enabled.

A workaround is to disable and enable them manually _AFTER_ isabelle has started up.

Change History (4)

comment:1 Changed 9 years ago by David Aspinall

Milestone: PG-Emacs-4.2PG-Emacs-4.3
Resolution: upstream
Status: newclosed

Confirmed, and thanks for reporting. But I believe this is a problem introduced inside Isabelle. If you look at the *isabelle* shell buffer, you see that Isabelle reports on start up to Proof General, e.g.

<haspref name="auto-quickcheck" descr="Run Quickcheck automatically." default="true"><pgipbool/>

which is intended to mean that the option is set by default inside Isabelle. But it isn't, as you've discovered.

(I guess this is what Makarius means by saying that Proof General for Isabelle is decaying while there isn't a maintainer on the Isabelle side looking after it.)

I'm closing this here as it needs to be fixed in Isabelle. Please could you report the problem to the Isabelle developers?

comment:2 Changed 9 years ago by Makarius

Cc: makarius@… added
Resolution: upstream
Status: closedreopened

To me it looks like the PGIP semantics have changed in recent years. In Proof General 3.x the "askprefs" default is not what the prover has at the moment, but the general static default. PG used to campare this somehow with his version and emit a full array of "setpref" messages to update all values on startup. The latter no longer happens in the PG-4.x line.

comment:3 Changed 9 years ago by Makarius

This has been repaired on the Isabelle side (after Isabelle2013): dismantling old PGIP implementations revealed what was actually happening, so it could be easily sorted out.

comment:4 Changed 9 years ago by Makarius

Resolution: fixed
Status: reopenedclosed
Note: See TracTickets for help on using tickets.