Proof Purger Interface: Difference between revisions
imported>Mathieu |
imported>Laurent →Selecting purge input: improved description of unused proofs |
||
| Line 9: | Line 9: | ||
Firstly, the proof purger tries to find unused proofs in the selection. | Firstly, the proof purger tries to find unused proofs in the selection. | ||
If | If no unused proof is found, a message will pop up telling that no proof needs to be purged. | ||
Otherwise, a new window will pop up displaying a list of all POs that are considered unused, | |||
that is all proofs that exist in some proof file and that do not have any corresponding proof obligation. | |||
==Choosing proofs to delete== | ==Choosing proofs to delete== | ||
Revision as of 16:39, 19 November 2010
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.
Selecting purge input
In any view, right-clicking an Event-B project or file will display a popup menu, containing a item. If several files or projects (or both) are selected, purging will apply to all of them.
Firstly, the proof purger tries to find unused proofs in the selection. If no unused proof is found, a message will pop up telling that no proof needs to be purged. Otherwise, a new window will pop up displaying a list of all POs that are considered unused, that is all proofs that exist in some proof file and that do not have any corresponding proof obligation.
Choosing proofs to delete
For the moment, nothing has been erased. The new window shows unused proofs and offers to choose among them which ones should be deleted. One may wish to keep some of them, knowing they might be useful in the future.
Once the selection has been decided, clicking the button will actually delete selected proofs from proof files. Files becoming empty will be deleted as well.
