The first step is to download Rodin. Rodin is available for download on the Rodin Download page. There is also a link for the download site in the faq (4.1.6).
Rodin is available for Windows, Mac OS, and Linux. For all the platforms, the distribution is always available for download as a zip file. Download the zip file for your system anywhere on your PC.
![]()
It is recommended that you download the latest stable version.
![]()
Rodin is easy to install on the platforms for which a prebuild version exists. If no prebuild version exists for your platform, please check out Section 4.1.8 in the FAQ on suggestions for how to install Rodin
To install Rodin, extract the contents of the zip file to a desired directory. You can run the tool by using the rodin executable.
Starting Rodin should bring up a welcome screen. It provides some quick guidance for Rodin. In particular, it provides instructions on installing the provers.
![]()
Please install the provers right away. It is easy and only takes a few clicks.
After dismissing the welcome screen, you should see the window shown in Figure 2.1. Here you can specify the path where Rodin stores your projects.
After specifying a path click the OK button. Rodin will start and the window shown in Figure 2.2 will open.
![]()
When using a Linux distribution, a welcome window may open up. Exit out of this window to get to the main screen. Other problems can also occur when installing Rodin in Linux. See the release notes for details.1
As already mentioned in Section 2.2.6, the GUI of an Eclipse application consists of views, editors, toolbars, quickviews, perspectives and many more elements. Here we list the different Rodin GUI elements (i.e. views) which are visible after starting Rodin for the first time and explain their functions:
The menu bar of the Rodin programs provides file and edit operations as well as other commands.
The tool bar provides short cuts for commonly used commands such as save, print, undo and redo.
The Event-B Explorer shows the projects’ tree structure. Projects are the main entries in this view, and when a project is expanded, the corresponding project files will also be shown.
The Outline view shows the outline of the active editor or file.
The Rodin Problems view displays problems (e.g., syntax errors) from the currently active projects.
The Symbols view shows a list of available mathematical symbols which can be used in conjunction with the mathematical notation (3.3).
The Editor view displays the active editor and is the view in which Event-B files are edited.
Footnotes