Proof Purger Design: Difference between revisions
imported>Mathieu |
imported>Nicolas No edit summary |
||
| Line 1: | Line 1: | ||
==Purpose== | ==Purpose== | ||
Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to allow the user to get rid of these proofs by selecting projects and/or files to purge. | Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to allow the user to get rid of these proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging. | ||
While this purging could be done automatically, proof files are considered to be owned by the user, so he alone can decide which proofs to delete or keep (he may need some of them in the future). | While this purging could be done automatically, proof files are considered to be owned by the user, so he alone can decide which proofs to delete or keep (he may need some of them in the future). | ||
| Line 22: | Line 22: | ||
First and third steps are cancellable operations based on the '''ProofPurger''' facilities, whereas the second is a selection dialog. | First and third steps are cancellable operations based on the '''ProofPurger''' facilities, whereas the second is a selection dialog. | ||
===Unused Proofs=== | ===Unused Proofs and Files=== | ||
User selection must first be filtered to get the files to search in. Selection may contain Event-B files or projects. All files of selected projects are considered selected as well. 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. | User selection must first be filtered to get the files to search in. Selection may contain Event-B files or projects. All files of selected projects are considered selected as well. 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 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, 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 38: | Line 42: | ||
===Purging=== | ===Purging=== | ||
Before deleting anything, selected proofs 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. | 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. | |||
[[Category:Design]] | [[Category:Design]] | ||
[[Category:Developer documentation]] | |||
Revision as of 16:28, 17 December 2008
Purpose
Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to allow the user to get rid of these proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging.
While this purging could be done automatically, proof files are considered to be owned by the user, so he alone can decide which proofs to delete or keep (he may need some of them in the future).
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
User selection must first be filtered to get the files to search in. Selection may contain Event-B files or projects. All files of selected projects are considered selected as well. 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.
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.
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.
