Bad behaviour in startup when proof executables (isabelle, isatool) not found

[David Aspinall]

If the workbench is started when an editor on a script file is open, the user is shown the dialog for entering a path, but the system repeatedly tries the broken path. If the workbench is started without an open editor, it hangs when the first editor is opened.

[David Aspinall]

Fixed repeated attempts to startup prover by using additional flag to SessionManager? constructor when displaying dialog. However, there is still a deadlock when the wizard is used to create a new theory file without finding the "isabelle" executable.

[David Aspinall]

Seems this change is not good enough: fetching a session manager is the main path for starting the prover now! What we can try to do is to keep a flag indicating whether the prover path is invalid, and not attempt to start the prover if this flag suggests it shouldn't be started. Probably also need a method to explicitly check/start prover before main actions, then popping up dialog is OK.

[David Aspinall]

Flawed patch to SessionManagerFactory?

[David Aspinall]

A different case: prover exits during startup. Set prover process to /bin/echo, click on Next button in a proof script. Triggers a couple of exceptions.

Searching for prover (/bin/echo): /bin/echo
Prover startup: -I -X (ignored)
java.lang.IllegalThreadStateException: process hasn't exited
	at java.lang.UNIXProcess.exitValue(UNIXProcess.java:172)
	at ed.inf.utils.process.ProcessUtils.waitFor(ProcessUtils.java:27)
	at ed.inf.proofgeneral.sessionmanager.SessionManager.noteStreamStopped(SessionManager.java:1786)
	at ed.inf.proofgeneral.sessionmanager.StreamGobbler.run(StreamGobbler.java:58)
java.lang.NullPointerException
	at ed.inf.proofgeneral.editor.actions.retargeted.GotoAction.goFwd(GotoAction.java:184)
	at ed.inf.proofgeneral.editor.actions.retargeted.GotoAction.run(GotoAction.java:156)
	at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
	at org.eclipse.ui.actions.RetargetAction.runWithEvent(RetargetAction.java:230)
	at org.eclipse.ui.internal.WWinPluginAction.runWithEvent(WWinPluginAction.java:234)
	at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:583)
	at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:500)
	at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)
	at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
	at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1158)
	at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3401)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3033)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2382)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2346)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2198)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:493)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:288)
	at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:488)
	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
	at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:193)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:382)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:549)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:504)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1236)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1212)
ACTION ERROR: null

[Graham Dutton]

Try as I might I cannot recreate this hang, either with plugin or product, either with an existing open editor or by starting afresh. I can reproduce an exception when there is no prover, but not so bad as the one reported.

I've tried using /bin/echo, an invalid file, and different scripts which never return, all to no avail.

[David Aspinall]

You're right, the hang does not occur now!! Perhaps because of fixing some problems with PGIP listeners and the command queue just yesterday. Good news.

I think the startup behaviour is now OK, although it would be good if the "15 seconds" dialog perhaps also popped up the settings dialog as the other case does (maybe optionally). The NPEs are still ugly though, so I think there is a case for a isProverAvailable() method in the SM which records whether the current prover setting is sensible (i.e. an executable file).

[David Aspinall]

Maybe an isLaunchable() method in ProverState?.java?

[Graham Dutton]

Preference dialog behaviour is much better with latest commit.

However, fixing the prover settings in response to one of these dialogs is not sufficient to regain prover functionality, even if a prover restart is triggered. Can't quite find the right place to reset state, but proverViable is not sufficient!

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted