Proof Purger Design: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Nicolas
New page: ==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 al...
 
imported>Mathieu
 
(6 intermediate revisions by 3 users not shown)
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.
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.


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).
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 22: Line 24:
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.
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.
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 38: Line 43:
===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.


Then proofs are deleted and files are saved.


Empty proof files are deleted, only if no associated PS file exists.
[[Category:Design]]
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.
[[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.

Popup menu extension

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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Proof_Purger_Design&oldid=6576’