Difference between revisions of "Proof Purger Interface"
imported>Laurent (→Selecting purge input: improved description of unused proofs) |
imported>Laurent (Replaced "unused" by "obsolete".) |
||
| Line 1: | Line 1: | ||
==Purpose== | ==Purpose== | ||
| − | Proofs are stored in proof files. | + | Proofs are stored in proof files. Each time a new proof obligation is generated |
| + | by the tool, a corresponding (initially empty) proof is created. However, | ||
| + | proofs are never removed automatically by the Rodin platform. As time passes | ||
| + | and a model is worked out, obsolete proofs (e.g., proofs that do not have a | ||
| + | corresponding proof obligation anymore) accumulate and clutter proof files. | ||
| + | |||
| + | The purpose of the proof purger is to allow the user to delete obsolete proofs. | ||
==Selecting purge input== | ==Selecting purge input== | ||
| − | In any view, right-clicking an Event-B project or file will display a popup menu, containing a {{menu|Purge Proofs...}} | + | In any view, right-clicking an Event-B project or file will display a popup |
| − | If several files or projects (or both) are selected, purging will apply to all of them. | + | menu, containing a {{menu|Purge Proofs...}} entry. If several files or projects |
| + | (or both) are selected, purging will apply to all of them. | ||
| − | Firstly, the proof purger tries to find | + | Firstly, the proof purger tries to find obsolete proofs in the selection. If |
| − | + | no obsolete proof is found, a message will pop up telling that no proof needs | |
| − | Otherwise, a new window will pop up displaying a list of all POs that are considered | + | to be purged. Otherwise, a new window will pop up displaying a list of all POs |
| − | that is all proofs that exist in some proof file and that do not have any corresponding proof obligation. | + | that are considered obsolete, 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== | ||
| Line 17: | Line 25: | ||
[[Image:selectProofsToDelete.jpg]] | [[Image:selectProofsToDelete.jpg]] | ||
| − | For the moment, nothing has been erased. The new window shows | + | For the moment, nothing has been erased. The new window shows obsolete 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|Delete}} button will | ||
| + | actually delete selected proofs from proof files. Files becoming empty will be | ||
| + | deleted as well. | ||
| + | |||
| + | ==Caution== | ||
| − | + | Proof purging shall not be performed on models that are not in a stable state. | |
| − | + | For instance, it should not be applied to a model that bears some errors or | |
| + | warnings issued by the type checker. This is because, in case of errors and | ||
| + | warnings, it can happen that not all proof obligations are generated. | ||
| + | Therefore, some proofs could be considered wrongly as obsolete. | ||
[[Category:User documentation]] | [[Category:User documentation]] | ||
[[Category:Proof]] | [[Category:Proof]] | ||
Revision as of 16:48, 19 November 2010
Purpose
Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However, proofs are never removed automatically by the Rodin platform. As time passes and a model is worked out, obsolete proofs (e.g., proofs that do not have a corresponding proof obligation anymore) accumulate and clutter proof files.
The purpose of the proof purger is to allow the user to delete obsolete proofs.
Selecting purge input
In any view, right-clicking an Event-B project or file will display a popup menu, containing a entry. If several files or projects (or both) are selected, purging will apply to all of them.
Firstly, the proof purger tries to find obsolete proofs in the selection. If no obsolete 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 obsolete, 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 obsolete 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.
Caution
Proof purging shall not be performed on models that are not in a stable state. For instance, it should not be applied to a model that bears some errors or warnings issued by the type checker. This is because, in case of errors and warnings, it can happen that not all proof obligations are generated. Therefore, some proofs could be considered wrongly as obsolete.
