Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
4.2.3 The builder takes too long
Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:
the first one is to disable the automated prover in the Preferences panel.
the second one is to mark a PO as reviewed if you do not want the auto-prover to attempt it anymore.
Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the Event-B Explorer.
To disable the automated prover, open Rodin Preferences (menu Window 
Preferences...). In the tree on the left-hand panel, select Event-B Sequent Prover Auto-tactic. Then, in the right-hand panel ensure that the checkbox labelled Enable auto-tactic for proving is disabled.
To review a proof obligation, just open it in the interactive prover and then click on the review button (this is a round blue button with a R in the proof control toolbar). The proof obligation should now labelled with the same icon in the Event-B explorer.
|
|
|
|
|
|