Menu
▾
▴
#413 Clean with AutoProve on works the second time
Project > Prove Automatically option turned on.
Import the attached project archive. The only PO is unattempted.
1st time:
Project > Clean... select the imported project => the PO is still unattempted
2nd time:
Project > Clean... select the imported project => the PO is discharged
Example
Pruning and saving the proof allows to repeat the problem.
Moreover, if the proof editor is still open with the pruned proof after the PO has been eventually discharged at 2nd clean, we are in an incoherent state: pruned proof in editor and discharged PO in the explorer.
At this stage, double clicking the PO in the explorer tries to open a new proof editor, which results in an unexpected error popup telling that the proof attempt already exists.
The error log gives 2 errors:
!ENTRY org.rodinp.core 4 2 2010-03-03 17:00:48.144
!MESSAGE Problems occurred when invoking code from plug-in: "org.rodinp.core".
!STACK 0
org.eclipse.swt.SWTException: Invalid thread access
at org.eclipse.swt.SWT.error(SWT.java:3884)
at org.eclipse.swt.SWT.error(SWT.java:3799)
at org.eclipse.swt.SWT.error(SWT.java:3770)
at org.eclipse.swt.widgets.Widget.error(Widget.java:450)
at org.eclipse.swt.widgets.Widget.checkWidget(Widget.java:389)
at org.eclipse.swt.widgets.Control.getVisible(Control.java:2559)
at org.eclipse.ui.internal.LayoutPart.getVisible(LayoutPart.java:243)
at org.eclipse.ui.internal.PartPane.setVisible(PartPane.java:308)
at org.eclipse.ui.internal.presentations.PresentablePart.setVisible(PresentablePart.java:180)
at org.eclipse.ui.internal.presentations.util.PresentablePartFolder.select(PresentablePartFolder.java:274)
at org.eclipse.ui.internal.presentations.util.PresentablePartFolder.remove(PresentablePartFolder.java:203)
at org.eclipse.ui.internal.presentations.util.LeftToRightTabOrder.remove(LeftToRightTabOrder.java:58)
at org.eclipse.ui.internal.presentations.util.TabbedStackPresentation.removePart(TabbedStackPresentation.java:461)
at org.eclipse.ui.internal.PartStack.remove(PartStack.java:867)
at org.eclipse.ui.internal.EditorSashContainer.removeEditor(EditorSashContainer.java:282)
at org.eclipse.ui.internal.EditorAreaHelper.closeEditor(EditorAreaHelper.java:84)
at org.eclipse.ui.internal.EditorAreaHelper.closeEditor(EditorAreaHelper.java:62)
at org.eclipse.ui.internal.WorkbenchPage.closeEditors(WorkbenchPage.java:1375)
at org.eventb.internal.ui.eventbeditor.EditorManager.closeRelatedEditors(EditorManager.java:98)
at org.eventb.internal.ui.eventbeditor.EditorManager.handleRemoveOperation(EditorManager.java:63)
at org.eventb.internal.ui.eventbeditor.EditorManager.handleDelta(EditorManager.java:56)
...
and
!ENTRY org.rodinp.core 4 4 2010-03-03 17:00:48.154
!MESSAGE Exception occurred in listener of Rodin element change notification
!STACK 0
org.eclipse.swt.SWTException: Invalid thread access
at org.eclipse.swt.SWT.error(SWT.java:3884)
at org.eclipse.swt.SWT.error(SWT.java:3799)
... idem
which looks like a concurrent access problem (we may have to put this into another bug if not directly related to the main problem).
This bug was fixed by the correction given to the bug #2976578 in r r8509. The exception raised while the .bps file was removed from the first clean operation. As an SWT exception was thrown right after that, the build process broke and the Prove Automatically could not be executed.
The first clean now discharge the PO.
Bug re-opened, as another scenario produces an issue:
Open a context file with one theorem, for example ⊤ ∨ ⊥.
When opening the proof, auto-tactics discharge the proof.
Then, prune the proof tree.
Perform Clean. The proof is not discharged.
At second clean, the proof is discharged.
The .bps file is not cleaned the first time, but is the second time.
The Rodin builder has been fixed: now it always cleans up generated files, even if they have been modified since the last build. Hence, the "bps" file is removed during clean and the automated prover is attempted in the subsequent build, which fixes the second scenario.
Change committed to Subversion (r8621).