Proof Dependencies and Reasoner Conflicts - Revision history

imported>Nicolas at 14:49, 6 June 2011

2011-06-06T14:49:39Z

← Older revision		Revision as of 14:49, 6 June 2011
Line 3:		Line 3:
	Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.		Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.

	This evolution is available since Rodin 2.2. It applies to all proofs edited using Rodin 2.2+. Proofs edited using previous versions of the tool are kept in the older format, thus slowing down the build time. ~~A plug-in is under development~~ to ~~allow~~ for ~~migrating old~~ proofs to the ~~new storage format~~.		This evolution is available since Rodin 2.2. It applies to all proofs edited using Rodin 2.2+. Proofs edited using previous versions of the tool are kept in the older format, thus slowing down the build time.

			In order to upgrade proof storage for proofs made using Rodin prior to 2.2, use '''Simplify Proof(s)''' on a proof or component or project.

			This works for reusable proofs, broken proofs need to be manually edited. (It will not actually make any modification as the simplification has been disabled since Rodin 2.0.)


	{{TODO\|Document proof storage}}		{{TODO\|Document proof storage}}

imported>Nicolas at 12:52, 1 June 2011

2011-06-01T12:52:03Z

← Older revision		Revision as of 12:52, 1 June 2011
Line 1:		Line 1:
	Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions.		Until Rodin 2.1 (included), proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions.

	Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.		Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.

			This evolution is available since Rodin 2.2. It applies to all proofs edited using Rodin 2.2+. Proofs edited using previous versions of the tool are kept in the older format, thus slowing down the build time. A plug-in is under development to allow for migrating old proofs to the new storage format.

	{{TODO\|Document proof storage}}		{{TODO\|Document proof storage}}

imported>Nicolas at 12:46, 1 June 2011

2011-06-01T12:46:46Z

← Older revision		Revision as of 12:46, 1 June 2011
Line 1:		Line 1:
	Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions.		Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions.
	Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.		Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.

			{{TODO\|Document proof storage}}

imported>Nicolas: New page: Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in rea...

2011-03-09T17:26:14Z

New page: Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in rea...

New page

Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions.
Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.