Proof Purger Interface - Revision history

imported>Ladenberger at 10:20, 27 October 2011

2011-10-27T10:20:00Z

← Older revision		Revision as of 10:20, 27 October 2011
Line 1:		Line 1:
	~~{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"~~
	\|-
	~~! scope="col" \| Do not edit! This content has been migrated to Subversion.~~
	\|-
	~~\|([http://handbook.event-b.org Nightly Handbook Build])~~
	\|}

	==Purpose==		==Purpose==

imported>Ladenberger at 12:26, 16 September 2011

2011-09-16T12:26:02Z

← Older revision		Revision as of 12:26, 16 September 2011
Line 1:		Line 1:
			{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"
			\|-
			! scope="col" \| Do not edit! This content has been migrated to Subversion.
			\|-
			\|([http://handbook.event-b.org Nightly Handbook Build])
			\|}

	==Purpose==		==Purpose==

imported>Laurent: Added rationale for obsolete proofs

2010-11-22T10:02:07Z

Added rationale for obsolete proofs

← Older revision		Revision as of 10:02, 22 November 2010
Line 8:		Line 8:

	The purpose of the proof purger is to allow the user to delete obsolete proofs.		The purpose of the proof purger is to allow the user to delete obsolete proofs.

			==Why proofs become obsolete==

			Proof obligations are named after the main elements related to it, such as
			events and invariants. Therefore, each time such an element is renamed
			manually, the corresponding proof obligations get a new name. However, the
			existing proof is not renamed, and a new proof gets created with the new name.

			Therefore, after a lot of model editing, there are more and more obsolete
			proofs stored in proof files.

	==Selecting purge input==		==Selecting purge input==

imported>Laurent: Replaced "unused" by "obsolete".

2010-11-19T16:48:10Z

Replaced "unused" by "obsolete".

← Older revision		Revision as of 16:48, 19 November 2010
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.		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...}} ~~item~~.		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 ~~unused~~ proofs in the selection.		Firstly, the proof purger tries to find obsolete proofs in the selection. If
	If no ~~unused~~ proof is found, a message will pop up telling that no proof needs to be purged.		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 ~~unused~~,		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 ~~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.		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==

	~~Once~~ the ~~selection has been decided~~, ~~clicking the {{button\|Delete}} button will actually delete selected proofs from~~ proof ~~files~~.		Proof purging shall not be performed on models that are not in a stable state.
	~~Files becoming empty will~~ be ~~deleted~~ as ~~well~~.		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]]

imported>Laurent: /* Selecting purge input */ improved description of unused proofs

2010-11-19T16:39:02Z

Selecting purge input: improved description of unused proofs

← Older revision		Revision as of 16:39, 19 November 2010
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 ~~none are~~ found, a message will ~~appear~~ telling that no proof needs to be purged.		If no unused proof is found, a message will pop up telling that no proof needs to be purged.
	~~Else~~, a new window will ~~show the result~~.		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==

imported>Mathieu: Category:Proof

2009-08-12T12:54:24Z

Category:Proof

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

	[[Category:User documentation]]		[[Category:User documentation]]
			[[Category:Proof]]

imported>Nicolas: Purging Unused Proofs moved to Proof Purger Interface: Clarify the intended aim of the document.

2009-01-06T16:04:33Z

Purging Unused Proofs moved to Proof Purger Interface: Clarify the intended aim of the document.

← Older revision	Revision as of 16:04, 6 January 2009
(No difference)

imported>Mathieu: Use some typesetting template

2008-12-11T21:55:20Z

Use some typesetting template

← Older revision		Revision as of 21:55, 11 December 2008
Line 5:		Line 5:
	==Selecting purge input==		==Selecting purge input==

	In any view, right-clicking an Event-B project or file will display a popup menu, containing a "Purge Proofs..." item.		In any view, right-clicking an Event-B project or file will display a popup menu, containing a {{menu\|Purge Proofs...}} item.
	If several files or projects (or both) are selected, purging will apply to all of them.		If several files or projects (or both) are selected, purging will apply to all of them.

Line 18:		Line 18:
	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.		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 "Delete" button will actually delete selected proofs from proof files.		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.		Files becoming empty will be deleted as well.

	[[Category:User documentation]]		[[Category:User documentation]]

imported>Mathieu: Category:User documentation

2008-12-11T21:49:00Z

Category:User documentation

← Older revision		Revision as of 21:49, 11 December 2008
Line 20:		Line 20:
	Once the selection has been decided, clicking the "Delete" button will actually delete selected proofs from proof files.		Once the selection has been decided, clicking the "Delete" button will actually delete selected proofs from proof files.
	Files becoming empty will be deleted as well.		Files becoming empty will be deleted as well.

			[[Category:User documentation]]

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:23:42Z

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.

==Selecting purge input==

In any view, right-clicking an Event-B project or file will display a popup menu, containing a "Purge Proofs..." 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 none are found, a message will appear telling that no proof needs to be purged.
Else, a new window will show the result.

==Choosing proofs to delete==

[[Image:selectProofsToDelete.jpg]]

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 "Delete" button will actually delete selected proofs from proof files.
Files becoming empty will be deleted as well.