Proof Purger Design - Revision history

imported>Mathieu: Category:Proof

2009-08-12T12:54:14Z

← Older revision		Revision as of 12:54, 12 August 2009
Line 49:		Line 49:

	[[Category:Design]]		[[Category:Design]]
			[[Category:Proof]]

imported>Laurent: /* Unused Proofs and Files */

2009-01-29T13:43:50Z

Unused Proofs and Files

← Older revision		Revision as of 13:43, 29 January 2009
Line 26:		Line 26:
	===Unused Proofs and Files===		===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.		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.

imported>Laurent: /* Purpose */

2009-01-29T13:40:25Z

Purpose

← Older revision		Revision as of 13:40, 29 January 2009
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. In addition, empty proof files are also proposed for purging~~.		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==

imported>Nicolas: Proof Purger moved to Proof Purger Design: Clarify the intended aim of the document.

2009-01-06T15:59:57Z

Proof Purger moved to Proof Purger Design: Clarify the intended aim of the document.

← Older revision	Revision as of 15:59, 6 January 2009
(No difference)

imported>Mathieu: Category:Developer documentation is parent category of Design

2008-12-18T10:47:57Z

Category:Developer documentation is parent category of Design

← Older revision		Revision as of 10:47, 18 December 2008
Line 48:		Line 48:

	[[Category:Design]]		[[Category:Design]]
	~~[[Category:Developer documentation]]~~

imported>Nicolas at 16:28, 17 December 2008

2008-12-17T16:28:59Z

← Older revision		Revision as of 16:28, 17 December 2008
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.

	~~Then proofs are deleted and files are saved.~~

	~~Empty proof files are deleted, only if 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.
	[[Category:Design]]		[[Category:Design]]
			[[Category:Developer documentation]]

imported>Mathieu: Category:Design

2008-12-11T21:47:25Z

Category:Design

← Older revision		Revision as of 21:47, 11 December 2008
Line 44:		Line 44:
	Empty proof files are deleted, only if no associated PS file exists.		Empty proof files are deleted, only if 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, 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:Design]]

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...

2008-12-10T17:12:23Z

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...

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 allow the user to get rid of these proofs by selecting projects and/or files to purge.

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).

==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===

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.

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 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 are deleted and files are saved.

Empty proof files are deleted, only if 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.