Rodin Handbook


4.3.14 How can I save a Context or a Machine?

Once a machine or context is (partially) edited, you can save it by using the save button as indicated in Figure 4.3.

Figure 4.3: Save a context or a machine

Once a “Save" has been completed, three tools are called automatically, these are:

  • the Static Checker

  • the Proof Obligation generator (3.2.7)

  • the Auto-Prover (

This can take some time. A “Progress” view can be opened at the bottom right of the screen to see which tools are working (most of the time, it will be the auto-prover). This is done via Window $\rangle $ Show View $\rangle $ Progress.