Rodin Handbook





 
Previous: How do I install external plugins without using the Eclipse Update Manager? Up: General Tool Usage Next: What are the ASCII shortcuts for mathematical operators? Rodin User’s Handbook v.2.8

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.

Previous: How do I install external plugins without using the Eclipse Update Manager? Up: General Tool Usage Next: What are the ASCII shortcuts for mathematical operators?  
Rodin User’s Handbook v.2.8 : Frequently Asked Questions : General Tool Usage : The builder takes too long