Menu
▾
▴
#235 Unnecessary proof steps in the rebuild process
The problem is shown by the following steps:
1/ clean & rebuild the project
2/ modify a component
3/ the automatic prover is launch on totally unrelated component. The rebuild lasts much longer than necessary.
Laurent suggests also the following steps:
1/ create an new projetc with a single context
2/ add a simple theorem in this context (which is automatically prove)
3/ clean the project
4/ the proof is being unnecessarily reproved.
"Project -> Clean" has the following nasty feature, too: when both of the options "Clean projects selected below" and "Start a build immediately" are on, the resulting build activity may cover projects that have not been selected. The phenomenon is properly visible when some of the projects not selected have time-consuming proofs. The user may actually have had the intention to avoid time-consuming proofs by not selecting those projects.
This has now been fixed in CVS and will be available in the 0.9.1 release.
Now, the auto-prover is only attempted on a proof obligation that has changed and for which the attempt to reuse the previous proof (if any) has failed to discharge or review the new lemma.