How To Evolve Reasoners
A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour, or to match additional proof rules, even after the old implementation was used to prove models. This leads to various issues, from unexpected proving failures to global prover unsoundness.
This is why successive implementations of a reasoner have to be distinguished, so that proofs using older implementations get detected by the tool as broken.
But a reasoner evolution is sometimes conservative and does not require to consider proofs broken if they use the implementation of the reasoner prior to the evolution.
In order to deal with these various cases, notions of version and level have been defined.
This page is dedicated to explaining these notions and describing exactly what to do to keep the prover sound.
What happens if I do nothing ?
The consequences of doing nothing besides functional code changes entails that proofs made using old reasoner implementation will be left unnoticed. Thus, if we clean a project in order to update proof statuses, these proofs will be considered reusable (in the sense of org.eventb.core.seqprover.ProverLib.isProofReusable() ) and their status will be left unchanged, i.e potentially discharged even if the new reasoner implementation would fail where the older succeeded. But if we make a replay on these proofs, the new reasoner implementation will be used and the correct status will be found.
So we get a difference between reusability and replayability, which makes the prover globally unstable and potentially unsound.
Versions and Levels
TODO
How to decide what to do
TODO: make a decision tree and describe precisely what to do and how to proceed
