Rodin Handbook


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 shorten this process:

  • Disable the automated prover in the Preferences panel.

  • 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 $\rangle $ Preferences...). In the tree on the left-hand panel, select Event-B $\rangle $ Sequent Prover $\rangle $ Auto/Post-tactic. Then, in the main panel ensure that the checkbox labelled Enable auto-tactic for proving for proving is not selected.

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.