Proof Purger Design: Difference between revisions
imported>Mathieu m Category:Developer documentation is parent category of Design |
imported>Mathieu |
||
| (3 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
==Purpose== | ==Purpose== | ||
Both automated and interactive proofs are stored in the Rodin database. As proofs might have needed a lot of user effort to create, the Rodin platform takes care to ''never'' erase them. | |||
As a consequence of this shyness, proofs have a strong tendency to accumulate in user projects and can take a lot of space in the hard disk. A quick survey of existing projects showed that a lot of proofs were just lying around without user even being aware of their existence. | |||
The purpose of the proof purger is to allow users to explicitly request the deletion of unused proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging. | |||
==Popup menu extension== | ==Popup menu extension== | ||
| Line 24: | Line 26: | ||
===Unused Proofs and Files=== | ===Unused Proofs and Files=== | ||
The user selection must first be filtered to compute the list of files to search in. A selection may contain Event-B files or projects. All files of a selected project are considered as implicitly selected. In case a file and its parent project are both selected, the file plus all other project files are processed, just as if only the project was selected. | |||
Computing unused proofs consists in scanning all proofs and listing those having no PO sequent in the associated PO file. | Computing unused proofs consists in scanning all proofs and listing those having no corresponding PO sequent in the associated PO file. | ||
Unused proof files are empty proof files for which no associated PS file exists. | Unused proof files are empty proof files for which no associated PS file exists. | ||
This can be explained, as proof file might be empty on purpose (generated by the builder). An empty proof file becomes undesirable only after the component has been deleted. Component deletion does not affect the proof file, being considered a user file. So when the user requests purging, we must keep empty files of existing components and delete the others. The distinction is made by checking the existence of an associated PS file. | This can be explained, as proof file might be empty on purpose (generated by the builder). An empty proof file becomes undesirable only after the component has been deleted. Component deletion does not affect the proof file, the latter being considered a user file. So when the user requests purging, we must keep empty files of existing components and delete the others. The distinction is made by checking the existence of an associated PS file. | ||
If none are found, a message is shown and the action is complete. | If none are found, a message is shown and the action is complete. | ||
| Line 48: | Line 49: | ||
[[Category:Design]] | [[Category:Design]] | ||
[[Category:Proof]] | |||
Latest revision as of 12:54, 12 August 2009
Purpose
Both automated and interactive proofs are stored in the Rodin database. As proofs might have needed a lot of user effort to create, the Rodin platform takes care to never erase them.
As a consequence of this shyness, proofs have a strong tendency to accumulate in user projects and can take a lot of space in the hard disk. A quick survey of existing projects showed that a lot of proofs were just lying around without user even being aware of their existence.
The purpose of the proof purger is to allow users to explicitly request the deletion of unused proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging.
Integration of the proof purger as a popup menu is achieved in the manifest through the org.eclipse.ui.popupMenus extension point. As specified there, the proof purger action will be proposed when selected objects are of type IRodinElement.
The action class is FilePurgeAction.
Action
Purging is a three-step action:
- computing unused proofs inside the selection
- showing the user the result and letting him select proofs to delete
- actually deleting proofs
First and third steps are cancellable operations based on the ProofPurger facilities, whereas the second is a selection dialog.
Unused Proofs and Files
The user selection must first be filtered to compute the list of files to search in. A selection may contain Event-B files or projects. All files of a selected project are considered as implicitly selected. In case a file and its parent project are both selected, the file plus all other project files are processed, just as if only the project was selected.
Computing unused proofs consists in scanning all proofs and listing those having no corresponding PO sequent in the associated PO file.
Unused proof files are empty proof files for which no associated PS file exists. This can be explained, as proof file might be empty on purpose (generated by the builder). An empty proof file becomes undesirable only after the component has been deleted. Component deletion does not affect the proof file, the latter being considered a user file. So when the user requests purging, we must keep empty files of existing components and delete the others. The distinction is made by checking the existence of an associated PS file.
If none are found, a message is shown and the action is complete.
Selection dialog
Selection of proofs to delete is proposed in a simple checkbox tree viewer, following a "project > file > proof" hierarchy.
Class architecture is composed of the SelectionDialog containing the viewer, which is filled with data from the ContentProvider (for tree structure) and the LabelProvider (for node names).
Purging
Before deleting anything, selected proofs and files are verified, in case some of them would be used. This should not be possible as the dialog only offers to select among unused proofs; it is rather a safety check.
Then proofs and files are deleted, and modified files are saved.
